《嵌入式系统设计的验证与调试技术》系统介绍了适用于嵌入式系统设计整个生命周期的实用调试和验证技术,涵盖了嵌入式系统设计和各个主要的抽象层次。在掌握了本书介绍的大量的高度和验证技术后,读者可以构建出可靠的嵌入式系统和软件。
全书结构合理清晰,内容全面丰富,适合所有从事嵌入式研究与开发的专业人员阅读,同时对于模型验证方面的研究人员也具有重要的参考价值。

第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

本书的主要内容分为四大部分:**部分对应于第2章,主要介绍了嵌入式系统在模型层面上的功能验证,包括建模通用概念、模型测试、模型仿真、模型验证方法与工具等方面的内容;第二部分对应于第3章,主要介绍了嵌入式系统在实现级层面上的**通信验证,包括组件间通信主要的不兼容性和解决这些不兼容性的转换器实现方法与技术;第三部分对应于第4章,主要介绍了嵌入式系统在较低实现层面上的性能调试,包括程序执行时间的估计、导致执行时间不可预测的因素及其建模、系统级通信分析和执行时间可预测系统的设计等方面的内容;第四部分对应于第5章,主要介绍了嵌入式系统在较低实现层面上的功能调试,包括动态校验方法和形式化校核方法等方面的内容。该书可供各大专院校作为教材使用,也可供从事相关工作的人员作为参考用书使用。