嵌入式系统设计的验证与调试技术
2010-7
清华大学出版社
罗伊乔杜里
200
田尊华
无
21世纪是信息时代，尤其是计算机时代，也可以讲21世纪是嵌入式系统时代。从复杂的航天系统到简单的遥控器，无不与嵌入式系统相关。嵌入式系统已经与我们的日常生活密切相关，例如，移动电话、PDA、电子阅读器、各种家电、汽车、门禁系统、各种IC卡等等，可以讲，如果现在离开了嵌入式系统，我们的日常生活工作将无法正常进行。嵌入式计算就是在这种背景下提出来的，这也足以说明嵌入式系统的普及程度和重要性。 从安全可靠的角度来讲，嵌入式系统可以分为安全关键的(safety-critical)和非(或一般)安全关键的。属于安全关键的嵌入式系统有车辆、飞行、核电厂和医疗设备等方面的控制系统。属于非(或一般)安全关键的嵌入式系统有移动电话、HDTV、家电控制器等。不管嵌入式系统是否为安全关键的，可靠性都很重要。安全关键的系统出现问题可能意味着巨大的生命财产损失，而对于非(或一般)安全关键的嵌入式系统来说，出现问题时即便不会造成任何生命财产损失，也意味着对用户使用信心的打击，而这将直接关系到相关产品的市场前景。那么如何保证嵌入式系统和软件的可靠性呢?本书正是为此而编写。本书系统地讲述了嵌入式系统设计流程中各个阶段的验证问题。当然，根据嵌入式系统不同的安全需求，考虑到成本因素，在验证上可以区分对待。相比一般系统而言，对于安全关键的系统必须进行更加严格的验证。 本书的显著特征是针对嵌入式系统和软件这个特定的领域，从不同的层面系统地讨论了各种验证方法。本书具有的第二个特点是，与一般讲理论的书不同，本书在讲述过程中紧密结合具体示例(如空中交通管制系统和汽车控制系统)和标准案例(西门子基准测试套件中的代码段)。此外，本书还有针对性地给出了少而精的习题，为巩固相关知识和激发读者思考提供了良好的题材。 本书由国防科学技术大学的田尊华翻译，由肖国尊负责监督本书的翻译质量和进度。鉴于译者水平有限，时间仓促，不足和疏漏之处在所难免，敬请广大读者提供反馈意见。
《嵌入式系统设计的验证与调试技术》系统介绍了适用于嵌入式系统设计整个生命周期的实用调试和验证技术，涵盖了嵌入式系统设计和各个主要的抽象层次。在掌握了本书介绍的大量的高度和验证技术后，读者可以构建出可靠的嵌入式系统和软件。 全书结构合理清晰，内容全面丰富，适合所有从事嵌入式研究与开发的专业人员阅读，同时对于模型验证方面的研究人员也具有重要的参考价值。
罗伊乔杜里博士是新加坡国立大学的副教授，从纽约州立大学石溪分校获得了计算机科学的博士学位。他的研究方向为嵌入式软件和系统的建模与验证。Abhik发表了超过60篇论文及著作。他的研究成功地实现了针对嵌入式软件的可扩展的实用分析工具，用于提高软件的质量和程序员的
第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
（3）当A1℃的状态为预更新时，它会发送消息，引导所有连接的客户端获取新的天气信息，然后将自己的状态和客户端的状态都设置为更新（updating）。 （4）如果所有客户端报告成功获取新天气信息，那么ATC会发送消息通知这些客户端使用新的天气信息，然后将自己的状态和这些客户端的状态都设置为后更新（postupdating）。 否则，如果任何连接的客户端报告获取新天气信息失败，那么ATC会发送消息给所有的客户端，告诉它们使用自己原来的天气信息，然后将自己的状态和这些客户端的状态都设置为后恢复（postreverting）。 （5）当ATC的状态为后更新时，如果所有这些客户端都报告成功使用了新天气信息，那么更新就完成了。ATC会将自己的状态和这些客户端的状态设置为空闲，并重新将WCP设为启用。 否则，如果任何连接的客户端报告使用新天气信息失败，那么ATC会断开所有连接的客户端，重新将WCP设置为启用，并将自己的状态重新设置为空闲。 （6）当ATC的状态为后恢复时，如果所有的客户端都报告使用原天气信息成功，那么恢复过程就完成了。ATC会将自己的状态和这些客户端的状态都设置为空闲，并将WCP设为启用。 否则，如果任何连接的客户端报告使用原天气信息失败，那么.ATC会断开所有连接的客户端，重新将WCP设置为启用，并将自己的状态重新设置为空闲。 注释 前面的简化需求能够让人感觉到现实系统的需求文档，尽管这只是一个非常概略的需求。这个规范无疑是可以理解的，然而我们却不能直接通过它找出其中的错误。实际上刚才给出的这个非形式化规范存在死锁错误，即系统可能达到一个没有动作可以执行的状态。现在，我们继续研究能够检测、甚至有助于改正这类错误的建模概念和校验过程（基于这些建模概念）。
《嵌入式系统设计的验证与调试技术》特色： 《嵌入式系统设计的验证与调试技术》嵌入式系统软件验证方面的先驱之作。 针对嵌入式系统和软件这个特定的领域，从不同的层面系统地讨论了各种验证方法。 紧密结合具体示例和标准案例，并有针对性地给出了少而精的习题，为巩固相关知识和激发读者思考提供了良好的题材。
无
深度不够，那小小的书除了理论还能写些什么~~