本书主要介绍信息物理融合系统的基本理论，包括系统设计、规约、建模和分析方法。针对基于模型的设计、并发理论、分布式算法、规约和验证的形式化方法、控制理论、实时系统和混成系统等分支学科，从不同侧面对信息物理融合系统进行描述。本书采用数学化的建模、基于模型的设计，以及规约与分析等概念，并配以案例研究图解来阐述信息物理系统所涉及的分布式算法、网络协议、控制设计和机器人等理论。本书适合作为计算科学、计算机工程和电子工程相关学科的高年级本科生或一年级研究生的教材。
PrinciplesofCyber-PhysicalSystems信息物理融合系统由能够相互通信的计算设备组成，这些计算设备借助传感器和作动器实现与物理世界的交互。现实生活中，这样的系统越来越多，从智能建筑到医疗设备再到汽车都可以看作信息物理融合系统。在过去的十多年中，开发确保信息物理融合系统可靠性的设计和分析工具是一项具有挑战性的工作，它吸引了众多学术界和工业界的研究人员开展卓有成效的跨学科研究。
本书的目标是为信息物理融合系统的设计、规约、建模和分析提供一套基本理论，这些理论勾画了开发信息物理融合系统所涉及的众多分支学科，包括基于模型的设计方法、并发理论、分布式算法、规约和验证的形式化方法、控制理论、实时系统和混成系统。我试图为信息物理融合系统设计和分析方法相关的研究主题提供一套脉络清晰的理论思想。全书采用数学化的建模、规约与分析等概念，并配以案例研究图解来阐述信息物理系统所涉及的分布式算法、网络协议、控制设计和机器人等多学科分支理论。
本教材自成体系，适合作为计算科学、计算机工程和电子工程相关学科的高年级本科生或一年级研究生一学期课程的教材。第1章讨论了几种可供选择的课程组合。
我对信息物理融合系统的研究兴趣萌生于20世纪90年代和TomHenzinger合作研究混成系统协同性。另外，本教材的结构基于我与Tom合作撰写但未出版的课堂讲义《Computer-AidedVerification》（计算机辅助验证），其中，第２章和第３章中的一些例子和图例也来自该讲义，并得到Tom的同意。因此，Tom对本教材的贡献是不可估量的，我对他表达崇高的敬意。
我对信息物理融合系统的理解和本书的内容深受宾夕法尼亚大学工程学院RECISE信息物理融合系统研究中心的学生和同事的影响。在此，我对我的同事VijayKumar、InsupLee、RahulMangharam、GeorgePappas、LinhPhan、OlegSokolsky和UfukTopcu给予的合作与支持表示敬意。同时，我还要感谢DARPA和NSF在信息物理融合系统研究项目上对我的持续资助。
在过去的５年中，我已经勾画出了本教材的草稿，取名《PrinciplesofEmbeddedComputation》（嵌入式计算的基本原理），最初目标是在宾夕法尼亚大学开设一门嵌入式系统硕士研究生课程。定期教授这门课程是促使我完成本书的关键动因，学生的反馈也极大地促进了本教材内容的完善。感谢所有的学生和勤勉的助教，他们是SanjianChen、ZhihaoJiang、SalarMoarref、TruongNghiem、NimitSinghania和RahulVasist。
我也很幸运地收到了其他大学的研究者对本教材手稿的反馈建议。特别是根据SriramSankaranarayanan和PauloTabuada的建议，对第6章和第9章的内容进行了很多修改。特别感谢ChristosStergiou对最新版本进行了仔细的推敲，并对第9章的例子用Matlab工具进行模拟。
借此机会感谢出版商（MIT出版社）对本项目的支持，特别是VirginiaCrossman、MarieLufkinLee和MarcLowenthal在本书出版过程中提供了大量的帮助和鼓励。本书的写作耗时多年，如果没有家人的支持也是不可能完成的，我要特别感谢我妻子Mona的友善、爱和耐心。
RajeevAlur美国费城宾夕法尼亚大学2015年1月
译者序PrinciplesofCyber-PhysicalSystems进入21世纪，以计算机科学为代表的信息技术发展迅猛，一些代表新技术发展的计算技术名词泉涌而出，如物联网、互联网+、云计算、大数据、工业4.0等，而信息物理融合系统（Cyber-PhysicalSystem，CPS）是其中最为引人关注的技术热词之一。CPS作为一个正式的概念于2006年由美国国家自然基金委员会科学家HelenGates提出后，就被美国、欧盟和中国等各国政府定位为影响未来科技研究、国家信息技术与产业融合发展的国家战略目标，并制定了一系列的CPS技术研究和产业发展计划。
从技术上讲，CPS是为解决信息技术对传统产品数字化后所带来的问题进行的一次系统性思考。这些问题包括：数值计算误差积累、跨平台的计算时序性、开环控制的不确定性、分布式计算的网络时延、多核计算的调度性以及长生命周期产品的运维等。这些问题逐步成为一道阻碍新一代智能计算技术发展必须跨越的鸿沟。这就要求计算技术专家必须另辟计算科学的方法论和实践工程技术，指导工程技术人员在产品的策划和设计之初就用系统工程的观点，考虑贯穿于产品全生命周期的两类因素——物理过程和计算过程，以及它们之间的相互影响。
CPS技术的发展不仅要继承嵌入式系统、网络通信和控制论的技术和方法，同时还要对现有理论、技术框架进行突破和创新。CPS系统集成了计算过程和物理过程，并且物理过程与计算过程相互影响、深度融合。CPS的概念也指出了CPS的两条发展路径：物理系统的信息化和计算系统的物理化。这两条道路是将导致CPS的研究、开发和应用的多样化发展，还是将殊途同归、形成一套统一的理论和方法，还有待于广大的CPS技术研究开发人员通过进一步的努力来验证，我们将拭目以待。
本书从计算理论的角度总结了CPS技术必须考虑的理论方法，并综合了分布式控制和网络通信等相关技术，是一本系统介绍信息物理融合系统理论基础的教材或者工具书，不仅适合初学者，还适用于有相关经验的研究人员和工程技术人员。本书不但概述了信息物理融合系统的基本原理，而且详细介绍了对此类系统的规约、设计、建模和分析等一套理论，包括基于模型的设计方法、并发理论、分布式算法、形式化规约和验证方法、控制理论、实时系统和混成系统等，并配以案例分析来阐述信息物理系统所涉及的分布式算法、网络协议、控制设计和机器人等多学科分支理论。本书的选材和作为教材的特点在前言和第1章中已有详述，被世界名校采纳作为教材也充分说明了其价值，此处不再赘述。
本书的翻译主要由董云卫博士和张雨博士共同完成，西北工业大学嵌入式系统实验室的葛永琪、吴婷婷、魏晓敏、孙鹏鹏、贺媛媛、姜臻颖、魏昕和李峰等研究生也参与了本书的部分翻译和校对，他们为本书的出版付出了辛勤劳动。
由于中西方文化背景上的差异以及我们的学术和语言水平的限制，译文中难免有不妥甚至错误之处，欢迎读者及专家批评指正。
译者2016年10月1日于西安
目 录
Principles of Cyber-Physical Systems
出版者的话
译者序
前言
第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.2 LTL规约116
5.1.3 异步进程的LTL规约*118
5.1.4 超越LTL*121
5.2 模型检查122
5.2.1 Büchi自动机123
5.2.2 从LTL到Büchi自动机*126
5.2.3 嵌套深度优先搜索*130
5.2.4 符号重复性检查132
5.3 活性证明*136
5.3.1 eventuality属性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.3 PID控制器*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.2 EDF调度216
8.2.1 周期作业模型的EDF217
8.2.2 EDF的最优性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
书单推荐
