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

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

拉吉夫·阿卢尔(Rajeev Alur)，现为宾夕法尼亚大学计算机和信息科学Zisman Family教授，该校嵌入式系统硕士生课程主管。他于1991年获得斯坦福大学计算机科学博士学位，在1997年加入宾夕法尼亚大学之前，在贝尔实验室计算机科学研究中心工作。他的研究方向涉及计算机的3个子学科：理论计算机科学系统、系统设计的形式化方法、信息物理融合系统。他是ACM Fellow和DIEEE Fellow；并曾担任ACM SIGBED主席LICS大会主席。

出版者的话
译者序
前言
第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