信息物理融合系统导论PDF电子书下载

上篇：信息物理融合系统现状与分析 3

第1章 CPS简介 3

1.1 CPS概述 3

1.2 CPS与物联网、嵌入式系统、混成系统 5

1.2.1 CPS与物联网 6

1.2.2 CPS与嵌入式系统 8

1.2.3 CPS与混成系统 9

1.3 CPS的特点和挑战 10

1.4 国外研究现状 11

1.4.1 CPS模型 11

1.4.2 CPS数据传输与管理技术 13

1.4.3 CPS能源管理 13

1.4.4 CPS安全 14

1.4.5 CPS软件设计技术的研究现状 15

1.4.6 CPS控制技术的研究现状 15

1.4.7 面向具体应用的CPS研究现状 16

1.5 国内研究现状 19

1.6 本章小结 20

参考文献 21

第2章 CPS软件开发基础 25

2.1 引言 25

2.2 各种主流的CPS建模方法 26

2.2.1 基于信道和面向参与者的CPS建模 26

2.2.2 基于模态模型CPS建模 27

2.2.3 基于格本体的CPS建模 28

2.2.4 基于关联顺序的CPS建模 28

2.3 CPS规约方法 29

2.3.1 面向方面的规约方法 29

2.3.2 语义时间自动机 31

2.3.3 Hilbertean代数规约 32

2.4 CPS系统集成 33

2.4.1 CPS系统集成面临问题 33

2.4.2 CPS系统集成方法 34

2.5 CPS设计和开发方法 36

2.5.1 CPS设计的挑战 36

2.5.2 CPS设计需求 36

2.5.3 CPS开发方法 37

2.6 本章小结 39

参考文献 40

第3章 CPS关键属性分析 43

3.1 CPS的安全性 43

3.1.1 CPS安全需求 43

3.1.2 CPS安全的潜在威胁 44

3.1.3 CPS信息安全方案的主要机制 45

3.1.4 CPS安全性解决方案 47

3.1.5 CPS安全关键技术 48

3.2 CPS的可靠性 49

3.2.1 可靠性的定义 49

3.2.2 可靠性与安全性的区别 50

3.2.3 可靠性解决方案 51

3.3 CPS的可信性 53

3.3.1 CPS数据的可信性 53

3.3.2 CPS网络的可信性 54

3.3.3 CPS软件的可信性 55

3.3.4 CPS模块间的可信性 55

3.3.5 CPS中人的可信性 56

3.3.6 CPS可信性研究的重要性 56

3.3.7 电力CPS的可信性 57

3.4 本章小结 58

参考文献 58

第4章 CPS测试与验证 61

4.1 白盒测试 61

4.1.1 面向CPS硬件的白盒测试 61

4.1.2 面向CPS软件的白盒测试 62

4.1.3 面向CPS网络的白盒测试 63

4.1.4 面向CPS系统的白盒测试 64

4.2 黑盒测试 66

4.2.1 计算机系统测试 66

4.2.2 嵌入式系统测试 66

4.2.3 物联网和无线感知设备测试 67

4.2.4 实时性测试 68

4.2.5 CPS测试技术的现状 68

4.2.6 CPS测试技术面临的困难 69

4.3 CPS验证 70

4.3.1 验证的必要性 70

4.3.2 验证方法概述 71

4.3.3 验证模型 71

4.3.4 定理证明 73

4.3.5 模型检验 73

4.3.6 验证工具 76

4.4 本章小结 76

参考文献 76

第5章 CPS典型案例分析 80

5.1 智能交通系统 80

5.1.1 体系结构 81

5.1.2 智能交通CPS的主要构成 81

5.1.3 智能交通所涉及的关键技术 83

5.1.4 智能交通应用 83

5.1.5 面临的挑战 84

5.2 自主驾驶汽车 85

5.2.1 汽车CPS原理介绍 85

5.2.2 汽车CPS的实现 86

5.2.3 汽车CPS架构与应用 86

5.2.4 汽车远程信息服务系统 87

5.2.5 汽车导航 88

5.2.6 汽车安全系统 89

5.3 高速铁路安全监控系统 90

5.3.1 系统需完成的相关工作 90

5.3.2 系统的体系结构 90

5.3.3 安全监控系统的关键技术 92

5.3.4 未来的研究方向 93

5.4 智能电网 94

5.4.1 智能电网的产生背景 94

5.4.2 智能电网的含义 94

5.4.3 智能电网的特点与目标 95

5.4.4 智能电网的研究现状 97

5.4.5 智能电网的关键技术 100

5.5 智慧医疗 102

5.5.1 智慧医疗的现有基础架构 103

5.5.2 CPS推动医疗服务智能化 105

5.5.3 智慧医疗案例 109

5.6 本章小结 110

参考文献 111

第6章 CPS主要问题浅析 113

6.1 CPS信息流问题 113

6.1.1 信息流 113

6.1.2 CPS信息流的特殊性 114

6.1.3 CPS信息流模型 115

6.1.4 CPS中的信息流 116

6.1.5 信息流安全验证方法 118

6.2 离散和连续问题 119

6.3 时间同步问题 119

6.4 抽象体系问题 119

6.5 环境感知 120

6.6 多源、异构、海量数据的传输与处理 120

6.7 CPS的可验证性 121

6.8 软件工程方面 122

6.9 系统的安全性及可预测性 122

6.10 其他问题 123

6.11 本章小结 123

参考文献 124

下篇 信息物理融合系统建模与验证 129

第7章 CPS建模与验证研究概述 129

7.1 研究背景 129

7.2 研究现状 130

7.2.1 CPS建模相关研究 130

7.2.2 相关验证技术研究 131

7.3 存在的问题以及解决方法 137

7.4 本章小结 139

参考文献 139

第8章 微分动态逻辑与CPS验证 145

8.1 概述 145

8.2 微分动态逻辑 146

8.2.1 基本语法 146

8.2.2 HP元模型 149

8.2.3 微分动态逻辑验证方法 151

8.3 HybridUML建模 154

8.3.1 HybridUML语义基础：CHARON 154

8.3.2 HybridUML数学元模型 155

8.3.3 HybridUML规约补充 159

8.3.4 利用HybridUML建模过程 162

8.4 从HybridUML模型到HP模型转换 163

8.4.1 静态结构转换规则 164

8.4.2 动态行为转换规则 166

8.4.3 模型转换规则应用的模板 171

8.4.4 KeYmaera输入代码生成 172

8.5 模型转换一致性 173

8.6 实例分析 174

8.6.1 建模 174

8.6.2 模型转换与属性规约 176

8.7 属性验证 177

8.8 本章小结 181

参考文献 181

第9章 微分代数动态逻辑与CPS验证 185

9.1 微分代数动态逻辑 185

9.1.1 微分代数程序 185

9.1.2 DAL公式 187

9.1.3 基于DAL的属性规约与验证思想 188

9.2 基于HybridUML的CPS建模 190

9.2.1 HybridUML 191

9.2.2 扩展的HybridUML多元组 195

9.2.3 CPS建模 198

9.3 HybridUML模型向DAP转换 202

9.3.1 基本语义转换 203

9.3.2 系统模型转换 208

9.4 实例分析 213

9.4.1 空中避撞系统描述与建模 213

9.4.2 模型转换 217

9.4.3 DAL属性规约及推理验证 219

9.5 本章小结 221

参考文献 222

第10章 微分代数时序动态逻辑与CPS验证 226

10.1 微分代数时序动态逻辑 226

10.1.1 dTL和DAL公式比较 226

10.1.2 dTL和DAL语义比较 228

10.1.3 dTL和DAL相继式演算比较 232

10.2 CPS建模与属性验证 236

10.2.1 CPS建模 237

10.2.2 CPS属性规约 240

10.2.3 微分代数时序动态逻辑的语义 241

10.2.4 微分代数时序动态逻辑的相继式演算 245

10.3 实例分析 252

10.3.1 飞机避撞系统建模 252

10.3.2 飞机避撞系统安全性规约 255

10.3.3 飞机避撞系统安全性验证 255

10.4 本章小结 257

参考文献 257

第11章 QdL与CPS自适应性验证 261

11.1 概述 261

11.2 量化微分动态逻辑 262

11.2.1 基于QdL演算的属性验证 263

11.2.2 操作模型——QHP 264

11.2.3 QHP元模型 265

11.2.4 QHP代码格式 267

11.3 层次mode模型到QHP代码的转换 267

11.3.1 基于语义一致性的模型转换 268

11.3.2 QHP模型到QHP代码的转换 273

11.4 实例建模与验证 276

11.4.1 实例描述 277

11.4.2 HybridUML建模及QHP代码生成 278

11.4.3 自适应属性规约及验证 280

11.5 本章小结 284

参考文献 285

第12章 结束语 292

12.1 工作总结 292

12.2 工作展望 293

附录 缩略词表 294