| 本书的主要内容分为四大部分：第一部分对应于第2章，主要介绍了嵌入式系统在模型层面上的功能验证，包括建模通用概念、模型测试、模型仿真、模型验证方法与工具等方面的内容；第二部分对应于第3章，主要介绍了嵌入式系统在实现级层面上的高级通信验证，包括组件间通信主要的不兼容性和解决这些不兼容性的转换器实现方法与技术；第三部分对应于第4章，主要介绍了嵌入式系统在较低实现层面上的性能调试，包括程序执行时间的估计、导致执行时间不可预测的因素及其建模、系统级通信分析和执行时间可预测系统的设计等方面的内容；第四部分对应于第5章，主要介绍了嵌入式系统在较低实现层面上的功能调试，包括动态校验方法和形式化校核方法等方面的内容。该书可供各大专院校作为教材使用，也可供从事相关工作的人员作为参考用书使用。 |
| 罗伊乔杜里博士是新加坡国立大学的副教授，从纽约州立大学石溪分校获得了计算机科学的博士学位。他的研究方向为嵌入式软件和系统的建模与验证。Abhik发表了超过60篇论文及著作。他的研究成功地实现了针对嵌入式软件的可扩展的实用分析工具，用于提高软件的质量和程序员的效率。Abhik是软件工程和嵌入式系统方面许多大中型基金项目的首席研究员。他获得过多种奖项，包括IBM优秀员工奖和陈嘉庚青少年发明家奖。 |
| 第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 |
内容加载中，请稍后...
商品评论（0条）