信息物理融合系统(CPS)原理

    出版者的话
译者序
前言
第1章简介1
1.1什么是信息物理融合系统1
1.2信息物理融合系统的主要特征1
1.3研究主题概述3
1.4课程组织指南5
第2章同步模型8
2.1反应式构件8
2.1.1变量、值和表达式8
2.1.2输入、输出和状态9
2.1.3初始化9
2.1.4更新10
2.1.5执行11
2.1.6扩展状态机12
2.2构件属性13
2.2.1有限状态构件13
2.2.2复合构件14
2.2.3事件触发构件*14
2.2.4非确定性构件16
2.2.5输入使能构件17
2.2.6任务图和等待依赖关系18
2.3构件构成22
2.3.1方框图22
2.3.2输入／输出变量重命名23
2.3.3并行组合23
2.3.4输出隐藏29
2.4同步设计30
2.4.1同步电路30
2.4.2巡航控制系统33
2.4.3同步网络*36
参考文献说明38
第3章安全性需求40
3.1安全性规约40
3.1.1迁移系统的不变量40
3.1.2需求在系统设计中的作用43
3.1.3安全监控器46
3.2验证不变量48
3.2.1证明不变量48
3.2.2不变量的自动验证*52
3.2.3基于模拟的分析54
3.3枚举搜索*55
3.4符号搜索60
3.4.1符号迁移系统60
3.4.2符号广度优先搜索63
3.4.3约简有序二叉判定图*67
参考文献说明75
第4章异步模型77
4.1异步进程77
4.1.1状态、输入和输出77
4.1.2输入、输出和内部动作78
4.1.3执行80
4.1.4扩展的状态机82
4.1.5进程操作83
4.1.6安全性需求87
4.2异步设计原语88
4.2.1阻塞同步与非阻塞同步88
4.2.2死锁88
4.2.3共享存储器90
4.2.4公平性假设*95
4.3异步协调协议100
4.3.1领导选举100
4.3.2可靠传输103
4.3.3等待无关共识*105
参考文献说明110
第5章活性需求111
5.1时序逻辑111
5.1.1线性时序逻辑111
5.1.2LTL规约116
5.1.3异步进程的LTL规约*118
5.1.4超越LTL*121
5.2模型检查122
5.2.1Büchi自动机123
5.2.2从LTL到Büchi自动机*126
5.2.3嵌套深度优先搜索*130
5.2.4符号重复性检查132
5.3活性证明*136
5.3.1eventuality属性136
5.3.2条件response属性137
参考文献说明140
第6章动态系统142
6.1连续时间模型142
6.1.1连续变化的输入和输出142
6.1.2扰动模型148
6.1.3构件构成148
6.1.4稳定性149
6.2线性系统151
6.2.1线性度152
6.2.2线性微分方程的解154
6.2.3稳定性159
6.3控制器设计161
6.3.1开环控制器与反馈控制器162
6.3.2稳定化控制器162
6.3.3PID控制器*165
6.4分析技术*170
6.4.1数值模拟170
6.4.2栅栏函数172
参考文献说明176
第7章时间模型177
7.1时间进程177
7.1.1基于时间的电灯开关177
7.1.2有界延迟的缓冲器178
7.1.3多个时钟179
7.1.4形式化模型180
7.1.5时间进程组合182
7.1.6不完全时钟的建模184
7.2基于时间的协议184
7.2.1基于时间的分布式协调184
7.2.2音频控制协议186
7.2.3双腔植入式心脏起搏器190
7.3时间自动机194
7.3.1时间自动机的模型194
7.3.2区域等价*195
7.3.3基于矩阵表示的符号分析201
参考文献说明207
第8章实时调度208
8.1调度概念208
8.1.1调度器架构208
8.1.2周期作业模型209
8.1.3可调度性211
8.1.4其他的作业模型215
8.2EDF调度216
8.2.1周期作业模型的EDF217
8.2.2EDF的最优性219
8.2.3基于利用率的可调度性测试220
8.3固定优先级调度223
8.3.1单调截止期策略和单调速率策略223
8.3.2单调截止期策略的最优性*225
8.3.3单调速率策略的可调度性测试*229
参考文献说明234
第9章混成系统235
9.1混成动态模型235
9.1.1混成进程235
9.1.2进程组合239
9.1.3奇诺行为241
9.1.4稳定性243
9.2混成系统设计244
9.2.1自动驾驶车辆244
9.2.2多机器人协调的障碍规避246
9.2.3多跳控制网络*251
9.3线性混成自动机*256
9.3.1追赶游戏例子256
9.3.2形式化模型258
9.3.3符号可达性分析260
参考文献说明266
参考文献267
索引274

    本书主要介绍信息物理融合系统的基本理论，包括系统设计、规约、建模和分析方法。针对基于模型的设计、并发理论、分布式算法、规约和验证的形式化方法、控制理论、实时系统和混成系统等分支学科，从不同侧面对信息物理融合系统进行描述。本书采用数学化的建模、基于模型的设计，以及规约与分析等概念，并配以案例研究图解来阐述信息物理系统所涉及的分布式算法、网络协议、控制设计和机器人等理论。本书适合作为计算科学、计算机工

    前  言Principles of Cyber-Physical Systems信息物理融合系统由能够相互通信的计算设备组成，这些计算设备借助传感器和作动器实现与物理世界的交互。现实生活中，这样的系统越来越多，从智能建筑到医疗设备再到汽车都可以看作信息物理融合系统。在过去的十多年中，开发确保信息物理融合系统可靠性的设计和分析工具是一项具有挑战性的工作，它吸引了众多学术界和工业界的研究人员开展卓有成效的跨学科研究。    本书的目标是为信息物理融合系统的设计、规约、建模和分析提供一套基本理论，这些理论勾画了开发信息物理融合系统所涉及的众多分支学科，包括基于模型的设计方法、并发理论、分布式算法、规约和验证的形式化方法、控制理论、实时系统和混成系统。我试图为信息物理融合系统设计和分析方法相关的研究主题提供一套脉络清晰的理论思想。全书采用数学化的建模、规约与分析等概念，并配以案例研究图解来阐述信息物理系统所涉及的分布式算法、网络协议、控制设计和机器人等多学科分支理论。    本教材自成体系，适合作为计算科学、计算机工程和电子工程相关学科的高年级本科生或一年级研究生一学期课程的教材。第1章讨论了几种可供选择的课程组合。    我对信息物理融合系统的研究兴趣萌生于20世纪90年代和Tom Henzinger合作研究混成系统协同性。另外，本教材的结构基于我与Tom合作撰写但未出版的课堂讲义《Computer-Aided Verification》（计算机辅助验证），其中，第２章和第３章中的一些例子和图例也来自该讲义，并得到Tom的同意。因此，Tom对本教材的贡献是不可估量的，我对他表达崇高的敬意。    我对信息物理融合系统的理解和本书的内容深受宾夕法尼亚大学工程学院RECISE信息物理融合系统研究中心的学生和同事的影响。在此，我对我的同事Vijay Kumar、Insup Lee、Rahul Mangharam、George Pappas、Linh Phan、Oleg Sokolsky和Ufuk Topcu给予的合作与支持表示敬意。同时，我还要感谢DARPA和NSF在信息物理融合系统研究项目上对我的持续资助。    在过去的５年中，我已经勾画出了本教材的草稿，取名《Principles of Embedded Computation》（嵌入式计算的基本原理），最初目标是在宾夕法尼亚大学开设一门嵌入式系统硕士研究生课程。定期教授这门课程是促使我完成本书的关键动因，学生的反馈也极大地促进了本教材内容的完善。感谢所有的学生和勤勉的助教，他们是Sanjian Chen、 Zhihao Jiang、 Salar Moarref、Truong Nghiem、 Nimit Singhania和Rahul Vasist。    我也很幸运地收到了其他大学的研究者对本教材手稿的反馈建议。特别是根据Sriram Sankaranarayanan和Paulo Tabuada的建议，对第6章和第9章的内容进行了很多修改。特别感谢Christos Stergiou对最新版本进行了仔细的推敲，并对第9章的例子用Matlab工具进行模拟。    借此机会感谢出版商（MIT出版社）对本项目的支持，特别是Virginia Crossman、Marie Lufkin Lee和Marc Lowenthal在本书出版过程中提供了大量的帮助和鼓励。本书的写作耗时多年，如果没有家人的支持也是不可能完成的，我要特别感谢我妻子Mona的友善、爱和耐心。    Rajeev Alur美国费城宾夕法尼亚大学2015年1月