嵌入式系统设计的验证与调试技术

第1章 嵌入式系统验证简介/1
第2章 模型验证/5
2.1 平台与系统行为/6
2.2 模型设计准则/8
2.3 非形式化需求：案例分析/9
2.3.1 需求文档/10
2.3.2 非形式化需求简化/11
2.4 通用建模概念/13
2.4.1 有限状态机/13
2.4.2 FSM通信/16
2.4.3 基于消息顺序图的模型/22
2.5 建模概念讨论/31
2.6 模型仿真/33
2.6.1 FSM仿真/35
2.6.2 基于MSC的系统模型仿真/39
2.7 基于模型的测试/43
2.8 模型校验/50
2.8.1 属性规范/50
2.8.2 校验过程/63
2.9 SPIN验证工具/71
2.10 SMV验证工具/74
2.11 案例分析：空中交通管制器/77
2.12 参考文献/79
2.13 习题/80
第3章 通信验证/83
3.1 常见不兼容性/86
3.1.1 以不同的顺序发送/接收信号/86
3.1.2 处理不同的信号字母表/87
3.1.3 数据格式不匹配/89
3.1.4 数据率不匹配/91
3.2 转换器合成/92
3.2.1 本地协议和转换器的表示/92
3.2.2 转换器合成的基本思想/94
3.2.3 各种协议转换策略/100
3.2.4 避免不推进循环/101
3.2.5 避免死锁的投机传输/102
3.3 改变工作设计/105
3.4 参考文献/106
3.5 习题/107
第4章 性能验证/109
4.1 传统时间抽象/110
4.2 预测程序执行时间/114
4.2.1 WCET计算/116
4.2.2 微体系结构建模/127
4.3 处理单元内部的干扰/135
4.3.1 来自环境的中断/135
4.3.2 竞争与抢占/137
4.3.3 共享处理器缓存/141
4.4 系统级通信分析/144
4.5 设计可预测时间的系统/147
4.5.1 中间结果存储器/147
4.5.2 时间触发通信/152
4.6 新兴应用/154
4.7 参考文献/154
4.8 习题/155
第5章 功能验证/157
5.1 动态或基于轨迹的校验/159
5.1.1 动态切片/163
5.1.2 错误定位/171
5.1.3 导引测试方法/177
5.2 形式化校核/180
5.2.1 谓词抽象/183
5.2.2 通过谓词抽象进行软件校验/189
5.2.3 形式化校核与测试的结合/195
5.3 参考文献/198
5.4 习题/199