STALLOY：一种时空建模与分析语言
| 摘要 | 第6-7页 |
| ABSTRACT | 第7-8页 |
| 第一章 绪论 | 第12-18页 |
| 1.1 选题背景与意义 | 第12-14页 |
| 1.2 相关研究 | 第14-16页 |
| 1.3 论文研究内容 | 第16-17页 |
| 1.4 论文组织结构 | 第17-18页 |
| 第二章 Alloy与空间、时态逻辑相关理论介绍 | 第18-29页 |
| 2.1 Alloy语言概述 | 第18-21页 |
| 2.2 空间逻辑 | 第21-25页 |
| 2.2.1 度量空间和拓扑空间 | 第21-22页 |
| 2.2.2 基于拓扑空间的逻辑 | 第22-25页 |
| 2.3 时态逻辑 | 第25-26页 |
| 2.4 空间、时态逻辑组合规则 | 第26-27页 |
| 2.5 本章小结 | 第27-29页 |
| 第三章 时空操作符与时空关系 | 第29-34页 |
| 3.1 时空操作符 | 第29-30页 |
| 3.1.1 空间操作符 | 第29-30页 |
| 3.1.2 时态操作符 | 第30页 |
| 3.2 时空关系 | 第30-33页 |
| 3.2.1 空间关系 | 第30-32页 |
| 3.2.2 时态关系 | 第32-33页 |
| 3.3 本章小结 | 第33-34页 |
| 第四章 时空建模与分析语言:STALLOY | 第34-47页 |
| 4.1 STALLOY的时空逻辑语法和语义 | 第34-38页 |
| 4.1.1 语法 | 第34-35页 |
| 4.1.2 语义 | 第35-38页 |
| 4.2 计算复杂度分析 | 第38-44页 |
| 4.2.1 基本分析 | 第38-39页 |
| 4.2.2 空间逻辑 | 第39-40页 |
| 4.2.3 时态逻辑 | 第40页 |
| 4.2.4 时空逻辑 | 第40-44页 |
| 4.3 时空系统模型的常见性质 | 第44-46页 |
| 4.3.1 安全性 | 第44-45页 |
| 4.3.2 活性 | 第45-46页 |
| 4.3.3 响应性 | 第46页 |
| 4.4 本章小结 | 第46-47页 |
| 第五章 STALLOY工具实现 | 第47-57页 |
| 5.1 时空逻辑实现 | 第47-53页 |
| 5.1.1 空间逻辑实现 | 第47-51页 |
| 5.1.2 时态逻辑实现 | 第51-52页 |
| 5.1.3 交互操作实现 | 第52-53页 |
| 5.2 工具实现 | 第53-56页 |
| 5.2.1 STALLOY的系统框架 | 第53-54页 |
| 5.2.2 STALLOY的主要流程 | 第54-56页 |
| 5.3 本章小结 | 第56-57页 |
| 第六章 案例研究:列车防护系统建模与验证 | 第57-69页 |
| 6.1 城市轨交列车防护系统概述 | 第57-58页 |
| 6.2 系统需求分析 | 第58-60页 |
| 6.3 系统建模与性质描述 | 第60-67页 |
| 6.3.1 列车防护系统建模 | 第60-66页 |
| 6.3.2 列车防护系统的性质描述 | 第66-67页 |
| 6.4 系统验证 | 第67-68页 |
| 6.5 本章小结 | 第68-69页 |
| 第七章 总结与展望 | 第69-71页 |
| 7.1 总结 | 第69-70页 |
| 7.2 进一步工作 | 第70-71页 |
| 参考文献 | 第71-76页 |
| 致谢 | 第76-77页 |
| 攻读硕士学位期间发表论文和科研情况 | 第77页 |
