嵌入式周期控制系统的建模与分析
| 摘要 | 第1-8页 |
| Abstract | 第8-13页 |
| 第一章 绪论 | 第13-29页 |
| ·嵌入式周期控制系统的特征与问题 | 第13-18页 |
| ·软件建模,分析与验证方法概述 | 第18-25页 |
| ·本文的选题和主要工作 | 第25-29页 |
| 第二章 SPARDL的框架 | 第29-49页 |
| ·建模语言 | 第29-39页 |
| ·规范描述语言 | 第39-48页 |
| ·本章小结 | 第48-49页 |
| 第三章 SPARDL的时间自动机模型 | 第49-73页 |
| ·价格时间自动机 | 第49-58页 |
| ·NPTA的概率模型检查 | 第58-62页 |
| ·模式图到PTA的映射 | 第62-72页 |
| ·本章小结 | 第72-73页 |
| 第四章 SPARDL的语义 | 第73-99页 |
| ·操作语义 | 第73-82页 |
| ·类型规则 | 第82-89页 |
| ·SPARDL的互模拟 | 第89-98页 |
| ·本章小结 | 第98-99页 |
| 第五章 模型仿真 | 第99-109页 |
| ·方法概述 | 第99-101页 |
| ·模式图 | 第101-105页 |
| ·控制流 | 第105-107页 |
| ·本章小结 | 第107-109页 |
| 第六章 概率模型检查 | 第109-123页 |
| ·概率语义 | 第109-118页 |
| ·验证区间时序逻辑 | 第118-120页 |
| ·本章小结 | 第120-123页 |
| 第七章 实现与试验 | 第123-131页 |
| ·SPARDL工具链的实现 | 第123-125页 |
| ·使用SPARDL建模 | 第125-127页 |
| ·概率模型检查 | 第127-130页 |
| ·本章小结 | 第130-131页 |
| 第八章 结束语 | 第131-135页 |
| ·相关工作比较 | 第131-134页 |
| ·进一步的工作 | 第134-135页 |
| 附录A 语法定义 | 第135-139页 |
| A.1 一些基本元素的产生式 | 第135-137页 |
| A.2 模式图的产生式 | 第137-138页 |
| A.3 区间时序逻辑公式的产生式 | 第138-139页 |
| 附录B 正文中定理的证明 | 第139-145页 |
| B.1 定理4.2.4的证明 | 第139-140页 |
| B.2 定理4.2 .5的证明 | 第140页 |
| B.3 定理4.2.6的证明 | 第140-141页 |
| B.4 定理4 .2.7的证明 | 第141页 |
| B.5 引理4.3.11的证明 | 第141-143页 |
| B.6 引理4.3.12的证明 | 第143-144页 |
| B.7 定理4.3.13的证明 | 第144-145页 |
| 参考文献 | 第145-157页 |
| 致谢 | 第157-159页 |
| 攻读博士学位期间发表论文和参与科研情况 | 第159-161页 |
