基于协同验证与混成关系的混成系统形式化分析验证
| 摘要 | 第6-8页 |
| ABSTRACT | 第8-10页 |
| 第一章 绪论 | 第17-29页 |
| 1.1 引言 | 第17-19页 |
| 1.2 相关工作 | 第19-26页 |
| 1.2.1 混成系统的建模 | 第19-21页 |
| 1.2.2 混成系统的分析与验证 | 第21-26页 |
| 1.3 主要贡献 | 第26-28页 |
| 1.4 论文结构 | 第28-29页 |
| 第二章 基本概念及准备知识 | 第29-41页 |
| 2.1 混成系统概念 | 第29-31页 |
| 2.2 程序统一理论 | 第31-34页 |
| 2.3 霍尔逻辑 | 第34-37页 |
| 2.4 可满足性模理论 | 第37-40页 |
| 2.5 本章小结 | 第40-41页 |
| 第三章 混成系统的协同验证 | 第41-91页 |
| 3.1 引言 | 第42-44页 |
| 3.2 混成自动机及可达性分析 | 第44-53页 |
| 3.2.1 混成自动机 | 第44-47页 |
| 3.2.2 混成自动机的语义 | 第47-48页 |
| 3.2.3 混成自动机示例 | 第48-50页 |
| 3.2.4 线性与仿射混成自动机 | 第50-52页 |
| 3.2.5 可达性分析 | 第52-53页 |
| 3.3 仿真建模语言 | 第53-56页 |
| 3.4 协同验证过程 | 第56-60页 |
| 3.5 屏蔽门系统分析 | 第60-77页 |
| 3.5.1 系统需求 | 第60-61页 |
| 3.5.2 初步模型 | 第61-68页 |
| 3.5.3 验证与仿真 | 第68-73页 |
| 3.5.4 模型优化 | 第73-77页 |
| 3.6 列车防碰撞分析 | 第77-87页 |
| 3.6.1 需求 | 第78-79页 |
| 3.6.2 仿真 | 第79-84页 |
| 3.6.3 验证 | 第84-87页 |
| 3.7 相关工作 | 第87-89页 |
| 3.8 本章小结 | 第89-91页 |
| 第四章 基于混成关系的混成系统验证 | 第91-121页 |
| 4.1 引言 | 第91-93页 |
| 4.2 建模语言 | 第93-95页 |
| 4.3 混成关系 | 第95-99页 |
| 4.4 HML程序断言设计 | 第99-103页 |
| 4.5 推理规则 | 第103-109页 |
| 4.6 案例分析 | 第109-119页 |
| 4.6.1 水位控制 | 第110-114页 |
| 4.6.2 列车防碰撞控制 | 第114-119页 |
| 4.7 本章小结 | 第119-121页 |
| 第五章 基于SMT的混成系统仿真与验证 | 第121-145页 |
| 5.1 引言 | 第121-123页 |
| 5.2 建模语言 | 第123-126页 |
| 5.3 模型转换 | 第126-136页 |
| 5.3.1 L_(RF)-公式 | 第126-128页 |
| 5.3.2 串行模型转换 | 第128-133页 |
| 5.3.3 并发模型转换 | 第133-135页 |
| 5.3.4 HML模型的动态转换 | 第135-136页 |
| 5.4 案例分析 | 第136-143页 |
| 5.4.1 连续控制 | 第137-140页 |
| 5.4.2 离散控制 | 第140-143页 |
| 5.5 本章小结 | 第143-145页 |
| 第六章 仿真与验证原型工具实现 | 第145-157页 |
| 6.1 工具框架 | 第145-146页 |
| 6.2 语言分析技术 | 第146-149页 |
| 6.3 原型工具的中间结果 | 第149-151页 |
| 6.4 混成系统案例展示 | 第151-156页 |
| 6.5 本章小结 | 第156-157页 |
| 第七章 总结与展望 | 第157-161页 |
| 7.1 总结 | 第157-158页 |
| 7.2 展望 | 第158-161页 |
| 附录A 共享轨道列车防碰撞系统HML程序代码 | 第161-163页 |
| 参考文献 | 第163-181页 |
| 致谢 | 第181-183页 |
| 攻读博士学位期间发表论文和参与科研情况 | 第183-185页 |
