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

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

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

第1章 嵌入式系统验证简介
第2章 模型验证
2.1 平台与系统行为
2.2 模型设计准则
2.3 非形式化需求：案例分析
2.3.1 需求文档
2.3.2 非形式化需求简化
2.4 通用建模概念
2.4.1 有限状态机
2.4.2 FSM通信
2.4.3 基于消息顺序图的模型
2.5 建模概念讨论
2.6 模型仿真
2.6.1 FSM仿真
2.6.2 基于MSC的系统模型仿真
2.7 基于模型的测试
2.8 模型校验
2.8.1 属性规范
2.8.2 校验过程
2.9 SPIN验证工具
2.10 SMV验证工具
2.11 案例分析：空中交通管制器
2.12 参考文献
2.13 习题

第3章 通信验证
3.1 常见不兼容性
3.1.1 以不同的顺序发送／接收信号
3.1.2 处理不同的信号字母表
3.1.3 数据格式不匹配
3.1.4 数据率不匹配
3.2 转换器合成
3.2.1 本地协议和转换器的表示
3.2.2 转换器合成的基本思想
3.2.3 各种协议转换策略
3.2.4 避免不推进循环
3.2.5 避免死锁的投机传输
3.3 改变工作设计
3.4 参考文献
3.5 习题

第4章 性能验证
4.1 传统时间抽象
4.2 预测程序执行时间
4.2.1 WCET计算
4.2.2 微体系结构建模
4.3 处理单元内部的干扰
4.3.1 来自环境的中断
4.3.2 竞争与抢占
4.3.3 共享处理器缓存
4.4 系统级通信分析
4.5 设计可预测时间的系统
4.5.1 中间结果存储器
4.5.2 时间触发通信
4.6 新兴应用
4.7 参考文献
4.8 习题

第5章 功能验证
5.1 动态或基于轨迹的校验
5.1.1 动态切片
5.1.2 错误定位
5.1.3 导引测试方法
5.2 形式化校核
5.2.1 谓词抽象
5.2.2 通过谓词抽象进行软件校验
5.2.3 形式化校核与测试的结合
5.3 参考文献
5.4 习题