基于UML-Promela的联锁软件形式化建模与验证

目录

声明

致谢

1 引言

1.1 研究背景及意义

1.2 国内外研究现状

1.2.1 国外研究现状

1.2.2 国内研究现状

1.2.3 研究现状总结

1.3 研究目的和内容

1.3.1 研究目的

1.3.2 研究内容

2 统一建模语言UML及形式化方法介绍

2.1 UML统一建模语言

2.1.1 UML概述

2.1.2 UML组成

2.2 形式化方法概述

2.3 模型验证工具SPIN

2.3.1 SPIN的工作原理

2.3.2 Promela 模型与线性时态逻辑

2.4 本章小结

3 计算机联锁系统UML模型设计

3.1 计算机联锁系统的功能需求分析

3.1.1 计算机联锁系统的整体框架

3.1.2 联锁进路控制过程分析

3.1.3 联锁其它控制过程分析

3.2 计算机联锁系统UML静态模型的建立

3.2.1 联锁系统UML用例图的建立

3.2.2 联锁系统UML类图的建立

3.3 计算机联锁系统UML动态模型的建立

3.3.1 联锁系统UML状态图的建立

3.3.2 联锁系统UML顺序图的建立

3.4 本章小结

4 UML模型到Promela 模型的转换

4.1 模型转换规则的制订

4.1.1 UML类图的转换规则

4.1.2 UML状态图的转换规则

4.1.3 UML顺序图的转换规则

4.2 模型转换工具的研制

4.2.1 UML模型输出

4.2.2 转换程序设计

4.4 本章小结

5 模型验证和仿真平台的搭建

5.1 联锁系统验证语句

5.1.1 安全系统分析

5.1.2 LTL验证语句的提取

5.2 验证过程及结果

5.3 计算机联锁系统仿真平台

5.3.1 仿真平台的设计与实现

5.3.2 仿真结果

5.4 本章小结

6 总结与展望

6.1 总结

6.2 展望

参考文献

附录 A

图索引

表索引

作者简历及攻读硕士/博士学位期间取得的研究成果

独创性声明

学位论文数据集