基于SPIN的UML模型验证技术的研究

论文摘要

统一建模语言(Unified Modeling Language,UML)作为面向对象的分析与设计方法的代表,已经获得了广泛的关注和研究,并在多个领域中有成功的应用。然而,由于UML作为一种符号化语言系统,其语义采用自然语言描述,缺乏精确的语义描述,因此,难以对UML模型进行分析验证以判断设计规范是否满足目标需求。模型验证是一种能够有效保证系统可信性质的自动验证技术,已被广泛地应用于工业界。如何将UML与模型验证二者有效的相结合,从而避免系统设计中的错误,提高软件的生产效率和质量已成为软件工程领域的研究热点。简单进程元语言解释器(Simple PROMELA Interpreter,SPIN)作为模型验证的一种开源工具,由于具有占用内存空间小,并保证程序能够按照原有的工作方式被高效地验证的特点,被普遍地应用于工业界和学术界,因此,本文主要研究基于SPIN的UML模型验证技术。论文首先介绍了形式化验证的方法,以及模型验证技术的原理、特点和过程,对模型验证工具SPIN的原理、输入语言PROMELA和优化技术作了详细的阐述;其次,通过对UML模型的结构和特点的分析,选取UML中类图、状态机图和协作图作为系统描述模型,根据验证的需要,结合类图和状态机图作为验证模型;然后,基于同态映射的方法,给出了UML验证模型到PROMELA模型的转换方法,并使用层次自动机描述状态机,定义了其形式化语义,将状态机图和类图的信息表示为相应的PROMELA模型,将UML的协作图信息描述为LTL公式并作为系统约束,使用模型验证工具SPIN验证UML模型所描述系统的正确性;最后,基于上述研究工作,设计并开发了UML模型自动转换验证工具UML2PROMELA。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 研究背景
• 1.2 论文的主要工作
• 1.2.1 研究目标
• 1.2.2 研究内容
• 1.3 本论文的组织结构
• 第二章 模型验证
• 2.1 模型验证概述
• 2.1.1 模型验证的基本概念和原理
• 2.1.2 模型验证的过程
• 2.1.3 模型验证优化技术
• 2.2 时态逻辑
• 2.2.1 线性时态逻辑
• 2.2.2 分支时态逻辑
• 2.3 模型验证工具SPIN
• 2.3.1 PROMELA语言
• 2.3.2 系统性质的描述
• 第三章 UML模型的验证
• 3.1 UML简介
• 3.2 UML组成结构
• 3.3 UML建模
• 3.4 UML模型的验证
• 第四章 UML模型到PROMELA模型的转换
• 4.1 UML验证模型到PROMELA模型的转换方法
• 4.2 UML状态机的语义描述
• 4.2.1 UML状态机的抽象语法
• 4.2.2 活动状态配置
• 4.2.3 RTC-step语义及模拟执行算法
• 4.3 UML验证模型在PROMELA中的表示
• 4.4 UML协作图在PROMELA中的表示
• 4.5 UML模型到PROMELA模型的转换算法
• 第五章 UML自动转换验证工具的设计与实现
• 5.1 工具的体系结构
• 5.2 工具的设计与实现
• 5.2.1 基本数据结构
• 5.2.2 工具的核心算法的实现
• 5.2.3 工具的用户界面及使用
• 5.3 实例应用
• 第六章 总结与展望
• 6.1 总结
• 6.2 进一步的工作
• 参考文献
• 攻读硕士期间发表的论文
• 致谢