![嵌入式实时系统 调度、分析和验证](https://cover.qianqiantushu.cc/63/s6546dec.jpg)
![嵌入式实时系统 调度、分析和验证](https://cover.qianqiantushu.cc/63/s6546dec.jpg)
嵌入式实时系统 调度、分析和验证PDF电子书下载
- 电子书积分:14 积分如何计算积分?
- 作 者:(美)阿尔伯特陈著
- 出 版 社:北京:北京航空航天大学出版社
- 出版年份:2015
- ISBN:9787512418714
- 页数:404 页
第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 RMA 58
3.4.2 PerfoRMAx 59
3.4.3 TimeWiz 59
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 二元决策图BDDs 101
4.6.2 符号模型检测器 104
4.7 实时CTL 105
4.7.1 最小和最大延迟 105
4.7.2 条件发生的最小和最大数量 107
4.7.3 非单位转移时间 108
4.8 可用的工具 109
4.9 历史回顾和相关研究 110
4.10 总结 112
习题 114
第5章 可视形式化、状态图和STATEMATE 116
5.1 状态图 117
5.1.1 状态图的基本功能 117
5.1.2 语义 120
5.2 活动图 121
5.3 模块图 121
5.4 STATEMATE 122
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和输入INPUT 223
10.3.3 规则部分——RULES 224
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_A 293
10.12.9 特殊形式A 293
10.12.10 特殊形式D和Algorithm_D 295
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
- 《云计算节能与资源调度》彭俊杰主编 2019
- 《物联网与嵌入式技术及其在农业上的应用》马德新 2019
- 《计算机自适应英语语用能力测试系统设计与效度验证 以TEM4词汇与语法题为例》张一鑫著 2019
- 《STM32嵌入式技术应用开发全案例实践=CASES PRACTICE OF STM32 EMBEDDED TECHNOLOGY APPLICATION AND DEVELOPMENT》苏李果 2020
- 《安全协议形式化分析与验证》肖美华著 2019
- 《嵌入式系统接口面向物联网与CPS设计=EMBEDDED SYSTEM INTERFACING DESIGN FOR THE INTERNET-OF-THINGS(IOT) AND CY》(美)玛里琳·沃尔夫著 2020
- 《基于ARM的嵌入式系统和物联网开发》(英)佩里·肖(Perry Xiao)著 2020
- 《雷达对抗及反对抗作战能力评估与验证=RADAR COUNTERMEASURE AND COUNTERCOUNTERMEASURE OPERATIONAL CAPABILITY EVALUA》张友益 2019
- 《安全协议实施安全性自动化分析与验证》孟博 2019
- 《基于多Agent系统的制造业生产调度模型研究》(中国)赵良辉 2019
- 《SQL与关系数据库理论》(美)戴特(C.J.Date) 2019
- 《魔法销售台词》(美)埃尔默·惠勒著 2019
- 《看漫画学钢琴 技巧 3》高宁译;(日)川崎美雪 2019
- 《优势谈判 15周年经典版》(美)罗杰·道森 2018
- 《社会学与人类生活 社会问题解析 第11版》(美)James M. Henslin(詹姆斯·M. 汉斯林) 2019
- 《海明威书信集:1917-1961 下》(美)海明威(Ernest Hemingway)著;潘小松译 2019
- 《迁徙 默温自选诗集 上》(美)W.S.默温著;伽禾译 2020
- 《上帝的孤独者 下 托马斯·沃尔夫短篇小说集》(美)托马斯·沃尔夫著;刘积源译 2017
- 《巴黎永远没个完》(美)海明威著 2017
- 《剑桥国际英语写作教程 段落写作》(美)吉尔·辛格尔顿(Jill Shingleton)编著 2019
- 《大学计算机实验指导及习题解答》曹成志,宋长龙 2019
- 《指向核心素养 北京十一学校名师教学设计 英语 七年级 上 配人教版》周志英总主编 2019
- 《大学生心理健康与人生发展》王琳责任编辑;(中国)肖宇 2019
- 《大学英语四级考试全真试题 标准模拟 四级》汪开虎主编 2012
- 《大学英语教学的跨文化交际视角研究与创新发展》许丽云,刘枫,尚利明著 2020
- 《北京生态环境保护》《北京环境保护丛书》编委会编著 2018
- 《复旦大学新闻学院教授学术丛书 新闻实务随想录》刘海贵 2019
- 《大学英语综合教程 1》王佃春,骆敏主编 2015
- 《大学物理简明教程 下 第2版》施卫主编 2020
- 《指向核心素养 北京十一学校名师教学设计 英语 九年级 上 配人教版》周志英总主编 2019