信息物理融合系统原理

●出版者的话
译者序
前言
章简介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.4LTL*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
分析技术*170
.1数值模拟170
.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