基于CPS的实时系统的面向方面的形式化验证方法
| 摘要 | 第1-6页 |
| ABSTRACT | 第6-8页 |
| 目录 | 第8-10页 |
| CONTENTS | 第10-12页 |
| 第一章 绪论 | 第12-16页 |
| ·研究背景 | 第12-13页 |
| ·研究现状 | 第13-14页 |
| ·研究意义 | 第14页 |
| ·主要工作 | 第14页 |
| ·组织结构 | 第14-16页 |
| 第二章 研究基础 | 第16-40页 |
| ·CPS概述 | 第16-18页 |
| ·CPS简介 | 第16-17页 |
| ·CPS和其他分布式系统 | 第17-18页 |
| ·VDM++概述 | 第18-31页 |
| ·VDM严格的规范 | 第19-20页 |
| ·VDM严格的证明 | 第20-21页 |
| ·VDM语言 | 第21-30页 |
| ·VDM++ | 第30-31页 |
| ·AOP概述 | 第31-40页 |
| ·关注点概述 | 第32-33页 |
| ·非功能需求与NFR框架 | 第33-34页 |
| ·关注点分离 | 第34-40页 |
| 第三章 面向方面的VDM++建模 | 第40-54页 |
| ·上下文关注点的分离 | 第40-48页 |
| ·基于上下文和特征的建模 | 第41-42页 |
| ·VDM++设计 | 第42-48页 |
| ·将方面引入到VDM++中 | 第48-52页 |
| ·面向方面的开发 | 第48-50页 |
| ·编织及证明责任 | 第50-52页 |
| ·讨论和结论 | 第52-54页 |
| 第四章 面向方面的VDM++模型的形式化验证 | 第54-70页 |
| ·空中交通管制的语音通信系统 | 第55-56页 |
| ·VCS 3020S的形式化模型 | 第56-59页 |
| ·系统的架构 | 第56-57页 |
| ·该系统的功能的一个实例 | 第57-59页 |
| ·验证系统 | 第59-64页 |
| ·覆盖分析的目标和过程 | 第59-60页 |
| ·测试用例的方面化和形式化 | 第60-63页 |
| ·覆盖分析结果 | 第63-64页 |
| ·在形式化模型中改变需求 | 第64-70页 |
| ·将修改的过程方面化和形式化 | 第64-65页 |
| ·改变需求的一个例子 | 第65-66页 |
| ·新的功能方面化地集成到形式化建模中 | 第66-68页 |
| ·测试用例覆盖和时间分析 | 第68页 |
| ·结果的总结 | 第68-70页 |
| 总结与展望 | 第70-72页 |
| 参考文献 | 第72-78页 |
| 攻读学位期间发表的论文 | 第78-82页 |
| 致谢 | 第82页 |
