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

目　录
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