下一代工业将建立在CPS之上,随着CPS技术的发展和普及,使用网络实现功能扩展的自动化设备无处不在,并将推动工业产品和技术的升级换代,极大地提高汽车、航空航天、国防、工业自动化、健康/医疗设备、重大基础设施等主要工业领域的竞争力。本书通过较为全面的介绍CPS理论和技术发展,为CPS在自动化装备的发展提供了一些借鉴和经验。本书可供从事UHFRFID空中接口技术研究设计、工程应用的人员参考。
样章试读
目录
前言
上篇:信息物理融合系统现状与分析
第1章CPS简介3
1.1CPS概述3
1.2CPS与物联网、嵌入式系统、混成系统5
1.2.1CPS与物联网6
1.2.2CPS与嵌入式系统8
1.2.3CPS与混成系统9
1.3CPS的特点和挑战10
1.4国外研究现状11
1.4.1CPS模型11
1.4.2CPS数据传输与管理技术13
1.4.3CPS能源管理13
1.4.4CPS安全14
1.4.5CPS软件设计技术的研究现状15
1.4.6CPS控制技术的研究现状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.3CPS规约方法29
2.3.1面向方面的规约方法29
2.3.2语义时间自动机31
2.3.3Hilbertean代数规约32
2.4CPS系统集成33
2.4.1CPS系统集成面临问题33
2.4.2CPS系统集成方法34
2.5CPS设计和开发方法36
2.5.1CPS设计的挑战36
2.5.2CPS设计需求36
2.5.3CPS开发方法37
2.6本章小结39
参考文献40
第3章CPS关键属性分析43
3.1CPS的安全性43
3.1.1CPS安全需求43
3.1.2CPS安全的潜在威胁44
3.1.3CPS信息安全方案的主要机制45
3.1.4CPS安全性解决方案47
3.1.5CPS安全关键技术48
3.2CPS的可靠性49
3.2.1可靠性的定义49
3.2.2可靠性与安全性的区别50
3.2.3可靠性解决方案51
3.3CPS的可信性53
3.3.1CPS数据的可信性53
3.3.2CPS网络的可信性54
3.3.3CPS软件的可信性55
3.3.4CPS模块间的可信性55
3.3.5CPS中人的可信性56
3.3.6CPS可信性研究的重要性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.5CPS测试技术的现状68
4.2.6CPS测试技术面临的困难69
4.3CPS验证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.2CPS推动医疗服务智能化105
5.5.3智慧医疗案例109
5.6本章小结110
参考文献111
第6章CPS主要问题浅析113
6.1CPS信息流问题113
6.1.1信息流113
6.1.2CPS信息流的特殊性114
6.1.3CPS信息流模型115
6.1.4CPS中的信息流116
6.1.5信息流安全验证方法118
6.2离散和连续问题119
6.3时间同步问题119
6.4抽象体系问题119
6.5环境感知120
6.6多源、异构、海量数据的传输与处理120
6.7CPS的可验证性121
6.8软件工程方面122
6.9系统的安全性及可预测性122
6.10其他问题123
6.11本章小结123
参考文献124
下篇:信息物理融合系统建模与验证
第7章CPS建模与验证研究概述129
7.1研究背景129
7.2研究现状130
7.2.1CPS建模相关研究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.2HP元模型149
8.2.3微分动态逻辑验证方法151
8.3HybridUML建模154
8.3.1HybridUML语义基础:CHARON154
8.3.2HybridUML数学元模型155
8.3.3HybridUML规约补充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.4KeYmaera输入代码生成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.2DAL公式187
9.1.3基于DAL的属性规约与验证思想188
9.2基于HybridUML的CPS建模190
9.2.1HybridUML191
9.2.2扩展的HybridUML多元组195
9.2.3CPS建模198
9.3HybridUML模型向DAP转换202
9.3.1基本语义转换203
9.3.2系统模型转换208
9.4实例分析213
9.4.1空中避撞系统描述与建模213
9.4.2模型转换217
9.4.3DAL属性规约及推理验证219
9.5本章小结221
参考文献222
第10章微分代数时序动态逻辑与CPS验证226
10.1微分代数时序动态逻辑226
10.1.1dTL和DAL公式比较226
10.1.2dTL和DAL语义比较228
10.1.3dTL和DAL相继式演算比较232
10.2CPS建模与属性验证236
10.2.1CPS建模237
10.2.2CPS属性规约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操作模型——QHP264
11.2.3QHP元模型265
11.2.4QHP代码格式267
11.3层次mode模型到QHP代码的转换267
11.3.1基于语义一致性的模型转换268
11.3.2QHP模型到QHP代码的转换273
11.4实例建模与验证276
11.4.1实例描述277
11.4.2HybridUML建模及QHP代码生成278
11.4.3自适应属性规约及验证280
11.5本章小结284
参考文献285
第12章结束语292
12.1工作总结292
12.2工作展望293
附录缩略词表294]]>