UML交互图的模型验证方法研究——UML交互图至Promela程序的转换

摘要

随着我国信息化建设的不断发展，软件系统的广泛应用，在国民经济的各行各业中发挥了越来越重要的作用。特别在一些重要领域如航空航天、地铁调度，对软件的可靠性要求特别高，软件设计上的一点缺陷，都可能导致灾难性后果，造成重大损失。如何确保这些系统的可靠性已经成为计算机科学与控制论领域共同关注的一个焦点问题。
　　 本论文主要研究了针对UML交互图的模型检测(Model Checking)方法，利用成熟的Spin模型检测工具，对UML模型进行形式化验证，以确保软件设计模型的正确性。论文首先介绍了模型检测理论，并着重分析了模型检验工具Spin功能和使用方法及其建模语言Promela的结构和语法。重点研究了UML顺序图的形式化表示方法，提出了UML顺序图到Promela语言转换规则和软件实现算法，并介绍了模型转换验证工具的设计和实现方法。
　　 将形式化验证结合到软件设计过程中，可以帮助设计人员尽早发现问题，提高模型的可靠性，减少由于设计错误带来的巨大损失。模型转换验证工具可以将UML顺序图自动转换生成Promela程序，并调用Spin工具进行模拟和验证。

目录

文摘

英文文摘

声明

第1章 绪论

1.1 课题背景

1.2 主要工作和目标

1.3 论文结构

第2章 形式化验证

2.1 模型检测

2.2 时态逻辑

2.3 Spin工具

2.4 Promela语言

第3章 软件建模

3.1 建模语言

3.2 交互模型

第4章 模型转换算法及软件实现

4.1 顺序图的形式化描述

4.2 转换为Promela程序

4.3 转换过程的软件实现

第5章 实例分析

5.1 建立UML顺序图

5.2 解析XML文档

5.3 生成Promela程序

5.4 顺序图模拟

5.5 顺序图验证

第6章 结论和下一步工作

6.1 结论

6.2 下一步工作

参考文献

致谢