图书介绍
嵌入式实时系统 调度、分析和验证PDF|Epub|txt|kindle电子书版本网盘下载
- （美）阿尔伯特陈著 著
- 出版社： 北京：北京航空航天大学出版社
- ISBN：9787512418714
- 出版时间：2015
- 标注页数：404页
- 文件大小：50MB
- 文件页数：422页
- 主题词：微型计算机－系统设计
PDF下载
下载说明
嵌入式实时系统 调度、分析和验证PDF格式电子书版下载
下载的文件为RAR压缩包。需要使用解压软件进行解压得到PDF格式图书。建议使用BT下载工具Free Download Manager进行下载,简称FDM(免费,没有广告,支持多平台）。本站资源全部打包为BT种子。所以需要使用专业的BT下载软件进行下载。如BitComet qBittorrent uTorrent等BT下载工具。迅雷目前由于本站不是热门资源。不推荐使用！后期资源热门了。安装了迅雷也可以迅雷进行下载！
（文件页数 要大于 标注页数，上中下等多册电子书除外）
注意：本站所有压缩包均有解压码： 点击下载压缩包解压工具
图书目录
第1章 简 介1
1.1 什么是时间2
1.2 仿真3
1.3 测试4
1.4 验证5
1.5 运行时期监测5
1.6 相关资源6
第2章 非实时系统的分析与验证8
2.1 符号逻辑8
2.1.1 命题逻辑8
2.1.2 谓词逻辑15
2.2 自动机和语言22
2.2.1 语言和表示22
2.2.2 有限自动机23
2.2.3 非定时系统的规范指定和验证25
2.3 历史回顾和相关研究29
2.4 总结30
习 题31
第3章 实时调度和调度性分析33
3.1 确定计算时间34
3.2 单处理器调度35
3.2.1 独立可抢占任务的调度35
3.2.2 不可抢占任务的调度47
3.2.3 带前后次序约束的不可抢占任务48
3.2.4 周期任务间的通信：确定的会合模型50
3.2.5 带临界区域的周期任务：核心化监测模型51
3.3 多处理器调度53
3.3.1 调度表示53
3.3.2 单实例任务调度54
3.3.3 周期任务调度56
3.4 可用的调度工具57
3.4.1 PERTS/RAPID RMA58
3.4.2 PerfoRMAx59
3.4.3 TimeWiz59
3.5 可用的实时操作系统60
3.6 历史回顾和相关研究61
3.7 总结62
习题67
第4章 有限状态系统的模型检测70
4.1 系统规范70
4.2 CLARKE-EMERSON-SISTLA模型检测器72
4.3 CTL的扩展76
4.4 应用76
4.5 用C实现的完整的CTL模型检测器程序79
4.6 符号化模型检测101
4.6.1 二元决策图BDDs101
4.6.2 符号模型检测器104
4.7 实时CTL105
4.7.1 最小和最大延迟105
4.7.2 条件发生的最小和最大数量107
4.7.3 非单位转移时间108
4.8 可用的工具109
4.9 历史回顾和相关研究110
4.10 总结112
习题114
第5章 可视形式化、状态图和STATEMATE116
5.1 状态图117
5.1.1 状态图的基本功能117
5.1.2 语义120
5.2 活动图121
5.3 模块图121
5.4 STATEMATE122
5.4.1 形式语言122
5.4.2 信息检索和文档122
5.4.3 代码的执行和分析122
5.5 可用的工具123
5.6 历史回顾和相关研究124
5.7 总结125
习 题126
第6章 实时逻辑、图论分析与模式图127
6.1 规范和安全声明127
6.2 事件-动作模型128
6.3 实时逻辑128
6.4 限制性RTL公式130
6.5 不可满足性的检测133
6.6 高效的不可满足性检测134
6.7 工业例子：美国航空航天局X-38机组返回舱137
6.7.1 X-38航空电子体系结构137
6.7.2 时序特性138
6.7.3 使用RTL进行时序和安全分析138
6.7.4 RTL规范138
6.7.5 将RTL表示转化成Presburger算术142
6.7.6 约束图的分析145
6.8 模式图规范语言145
6.8.1 模式146
6.8.2 转 移147
6.9 验证模式图规范的时间属性148
6.9.1 系统运算148
6.9.2 运算图149
6.9.3 时间属性149
6.9.4 节点之间的最小和最大距离150
6.9.5 终点和间隔的排除与纳入151
6.10 可用的工具152
6.11 历史回顾和相关研究152
6.12 总结152
习题155
第7章 利用时间自动机进行验证158
7.1 Lynch-Vaandrager自动机理论方法158
7.1.1 定时执行159
7.1.2 定时轨迹159
7.1.3 时间自动机的组合160
7.1.4 MMT自动机160
7.1.5 验证技术161
7.1.6 通过仿真证明时间界限163
7.2 Alur-Dill自动机理论方法163
7.2.1 非定时轨迹164
7.2.2 定时轨迹164
7.2.3 Alur-Dill时间自动机167
7.3 Alur-Dill域自动机和验证169
7.3.1 时钟域170
7.3.2 域自动机171
7.3.3 验证算法172
7.4 可用的工具173
7.5 历史回顾和相关研究174
7.6 总结175
习 题178
第8章 时间相关的Petri网179
8.1 非定时Petri网179
8.2 带有时间扩展的Petri网181
8.2.1 定时Petri网181
8.2.2 时间Petri网181
8.2.3 高阶定时Petri网184
8.3 时间ER网185
8.4 高阶Petri网的属性189
8.5 TPN网的Berthomieu-Diaz分析算法190
8.5.1 从状态类出发的变迁的可发生性确定191
8.5.2 导出可达类192
8.6 Milano研究团队的HLTPN分析方法193
8.7 可用的工具195
8.8 历史回顾和相关研究195
8.9 总结196
习 题199
第9章 进程代数200
9.1 非定时进程代数200
9.2 Milner的通信系统演算201
9.2.1 行为程序的直接等价202
9.2.2 行为程序的全等203
9.2.3 等价关系：互模拟203
9.3 定时进程代数204
9.4 通信共享资源的进程代数204
9.4.1 ACSR的语法205
9.4.2 ACSR的语义：操作规则206
9.4.3 机场雷达系统的例子210
9.5 分析和验证211
9.5.1 分析的例子213
9.5.2 VERSA的使用214
9.5.3 实用性215
9.6 与其他方法的关系215
9.7 可用的工具216
9.8 历史回顾和相关研究216
9.9 总结217
习 题218
第10章 基于命题逻辑规则系统的设计与分析219
10.1 实时决策系统219
10.2 实时专家系统221
10.3 基于命题逻辑规则的程序——EQL语言222
10.3.1 声明部分223
10.3.2 初始化部分——初始化INIT和输入INPUT223
10.3.3 规则部分——RULES224
10.3.4 输出部分226
10.4 状态空间表示228
10.5 计算机辅助设计工具230
10.6 分析问题237
10.6.1 有限域238
10.6.2 特殊形式：对于常量的相容性赋值，L和T不相交239
10.6.3 通用分析策略241
10.7 工业例子：航天飞机压力控制系统的低温氢压力故障处理过程分析242
10.8 综合问题252
10.8.1 调度基于等式规则程序的时间复杂性254
10.8.2 拉格朗日乘子法求解时间预算问题255
10.9 在ESTELLA中规定终止条件257
10.9.1 分析方法概述258
10.9.2 规定行为约束断言的工具260
10.9.3 用于Estella的与语境无关的语法267
10.10 两个工业例子272
10.10.1 为分析ISA专家系统而规定循环和退出条件272
10.10.2 为分析FCE专家系统而规定断言274
10.11 Estella——通用分析工具278
10.11.1 通用分析算法279
10.11.2 独立规则集的选择279
10.11.3 相容条件的检查283
10.11.4 循环退出条件的检查284
10.12 定量时序分析算法286
10.12.1 概述286
10.12.2 等式逻辑语言287
10.12.3 互斥和相容288
10.12.4 高阶依赖图289
10.12.5 程序执行和响应时间291
10.12.6 状态空间图292
10.12.7 响应时间分析问题和特殊形式293
10.12.8 特殊形式A和Algorithm_A293
10.12.9 特殊形式A293
10.12.10 特殊形式D和Algorithm_D295
10.12.11 通用分析算法302
10.12.12 一些证明304
10.13 历史回顾和相关研究308
10.14 总结310
习 题312
第11章 基于谓词逻辑规则系统的时序分析314
11.1 OPS5语言315
11.1.1 概述316
11.1.2 Rete网络318
11.2 CHENG-TSAI时序分析方法319
11.2.1 OPS5控制路径的静态分析319
11.2.2 终止分析321
11.2.3 时序分析335
11.2.4 静态分析336
11.2.5 WM生成338
11.2.6 实现和实验342
11.3 CHENG-CHEN时序分析方法345
11.3.1 介 绍345
11.3.2 OPS5程序的分类346
11.3.3 OPS5系统响应时间351
11.3.4 符号列表364
11.3.5 实验结果365
11.3.6 程序员辅助移除循环366
11.4 历史回顾和相关研究372
11.5 总结373
习 题376
第12章 基于规则系统的优化377
12.1 简介377
12.2 背景379
12.3 基本定义380
12.3.1 EQL程序380
12.3.2 基于EQL程序范例的实时决策系统执行模型381
12.3.3 状态空间表示法382
12.3.4 固定点的导出384
12.4 优化算法385
12.4.1 EQL（B）程序的分解385
12.4.2 最优状态空间图的导出386
12.4.3 优化EQL（B）程序的综合393
12.5 实验评估394
12.5.1 无循环的EQL（B）程序395
12.5.2 带循环的EQL（B）程序396
12.5.3 工业应用举例：综合状态评估专家系统的优化396
12.6 优化方法的评价398
12.6.1 优化方法的定性比较398
12.6.2 优化算法所需的EQL语言约束398
12.6.3 其他基于规则实时系统的优化399
12.7 历史回顾和相关研究400
12.8 总结401
习 题402
参考文献404