形式化与可视化相结合的嵌入式实时软件建模和验证
| 中文摘要 | 第1-4页 |
| ABSTRACT | 第4-7页 |
| 第一章 绪论 | 第7-11页 |
| ·研究背景 | 第7-8页 |
| ·研究内容及意义 | 第8-10页 |
| ·本文组织结构 | 第10-11页 |
| 第二章 形式化方法概述 | 第11-20页 |
| ·形式化描述 | 第11-14页 |
| ·形式化验证 | 第14-20页 |
| 第三章 可视化建模语言UML 及其扩展 | 第20-29页 |
| ·UML 概述 | 第20-25页 |
| ·UML2.0 基本组成 | 第21页 |
| ·UML2.0 视图分析 | 第21-23页 |
| ·UML2.0 扩展机制 | 第23-25页 |
| ·UML2.0 顺序图 | 第25页 |
| ·UML2.0 顺序图的时序扩展 | 第25-28页 |
| ·本章小结 | 第28-29页 |
| 第四章 实时顺序图的形式语义 | 第29-38页 |
| ·时间自动机概述 | 第29-32页 |
| ·时间自动机的定义 | 第29-30页 |
| ·时间自动机验证工具UPPAAL | 第30-32页 |
| ·UML2.0 顺序图到时间自动机的转换方法 | 第32-35页 |
| ·简单子片段 | 第32-33页 |
| ·组合片段 | 第33-35页 |
| ·复合子片段 | 第35页 |
| ·时间自动机的优化 | 第35-37页 |
| ·本章小结 | 第37-38页 |
| 第五章 实例研究 | 第38-55页 |
| ·电梯控制系统说明 | 第38页 |
| ·电梯控制系统的用例分析 | 第38-39页 |
| ·电梯控制系统的UML2.0 顺序图建模 | 第39-48页 |
| ·建立时间自动机模型 | 第48-53页 |
| ·需求验证 | 第53-54页 |
| ·本章小节 | 第54-55页 |
| 第六章 总结与展望 | 第55-57页 |
| ·本文工作总结 | 第55页 |
| ·下一步工作 | 第55-57页 |
| 参考文献 | 第57-61页 |
| 攻读硕士期间参加的科研项目及发表（录用）的论文 | 第61-62页 |
| 致谢 | 第62-63页 |
| 详细摘要 | 第63-66页 |
