- 作 者：（印）罗伊乔杜里著
- 出 版 社：北京：清华大学出版社
- 出版年份：2010
- ISBN：9787302230724
- 标注页数：202 页
- PDF页数：214 页
请阅读订购服务说明与试读!
订购服务说明
1、本站所有的书默认都是PDF格式，该格式图书只能阅读和打印，不能再次编辑。
2、除分上下册或者多册的情况下，一般PDF页数一定要大于标注页数才建议下单购买。【本资源214 ≥202页】
图书下载及付费说明
1、所有的电子图书为PDF格式，支持电脑、手机、平板等各类电子设备阅读；可以任意拷贝文件到不同的阅读设备里进行阅读。
2、电子图书在提交订单后一般半小时内处理完成,最晚48小时内处理完成。(非工作日购买会延迟)
3、所有的电子图书都是原书直接扫描方式制作而成。
第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