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

本书特色

《嵌入式系统设计的验证与调试技术》特色：《嵌入式系统设计的验证与调试技术》嵌入式系统软件验证方面的先驱之作。针对嵌入式系统和软件这个特定的领域，从不同的层面系统地讨论了各种验证方法。紧密结合具体示例和标准案例，并有针对性地给出了少而精的习题，为巩固相关知识和激发读者思考提供了良好的题材。

节选

相关资料

插图：（3）当A1℃的状态为预更新时，它会发送消息，引导所有连接的客户端获取新的天气信息，然后将自己的状态和客户端的状态都设置为更新（updating）。（4）如果所有客户端报告成功获取新天气信息，那么ATC会发送消息通知这些客户端使用新的天气信息，然后将自己的状态和这些客户端的状态都设置为后更新（postupdating）。否则，如果任何连接的客户端报告获取新天气信息失败，那么ATC会发送消息给所有的客户端，告诉它们使用自己原来的天气信息，然后将自己的状态和这些客户端的状态都设置为后恢复（postreverting）。（5）当ATC的状态为后更新时，如果所有这些客户端都报告成功使用了新天气信息，那么更新就完成了。ATC会将自己的状态和这些客户端的状态设置为空闲，并重新将WCP设为启用。否则，如果任何连接的客户端报告使用新天气信息失败，那么ATC会断开所有连接的客户端，重新将WCP设置为启用，并将自己的状态重新设置为空闲。（6）当ATC的状态为后恢复时，如果所有的客户端都报告使用原天气信息成功，那么恢复过程就完成了。ATC会将自己的状态和这些客户端的状态都设置为空闲，并将WCP设为启用。否则，如果任何连接的客户端报告使用原天气信息失败，那么.ATC会断开所有连接的客户端，重新将WCP设置为启用，并将自己的状态重新设置为空闲。注释前面的简化需求能够让人感觉到现实系统的需求文档，尽管这只是一个非常概略的需求。这个规范无疑是可以理解的，然而我们却不能直接通过它找出其中的错误。实际上刚才给出的这个非形式化规范存在死锁错误，即系统可能达到一个没有动作可以执行的状态。现在，我们继续研究能够检测、甚至有助于改正这类错误的建模概念和校验过程（基于这些建模概念）。

作者简介

作者：（印度）罗伊乔杜里（Abhik Roychoudhury） 译者：田尊华罗伊乔杜里（Abhik Roychoudhury），博士是新加坡国立大学的副教授，从纽约州立大学石溪分校获得了计算机科学的博士学位。他的研究方向为嵌入式软件和系统的建模与验证。Abhik发表了超过60篇论文及著作。他的研究成功地实现了针对嵌入式软件的可扩展的实用分析工具，用于提高软件的质量和程序员的效率。Abhik是软件工程和嵌入式系统方面许多大中型基金项目的首席研究员。他获得过多种奖项，包括IBM优秀员工奖和陈嘉庚青少年发明家奖。