基于时态逻辑的UML交互模型检测研究

论文摘要

统一建模语言(Unified Modeling Language,UML)是一种易理解、易描述、直观的可视化建模语言,它提供多种模型元素从系统的各个角度描述系统性质、功能及运行环境。基于UML的计算机软件系统的分析和设计已经广泛地应用于各个领域。UML交互模型从系统行为的角度细致、准确地刻画了计算机软件系统的交互行为,为程序开发人员及最终用户正确理解系统的交互行为提供了便捷、高效的可视化模型。对UML交互模型进行验证判断软件系统模型是否满足交互的性质成为一个重要的研究问题。模型检测(Model checking)是一种应用广泛的形式化自动验证技术,主要通过显式状态搜索或隐式不动点计算来验证系统的模态/命题性质。本文采用基于自动机理论框架下的时态逻辑模型验证检测技术,对UML2.0交互模型的模型检测进行了研究。为了对UML2.0交互模型进行有关性质的检测,首先应将UML2.0交互模型进行形式化的描述,使其转化为一种可以接受消息交换或系统状态变化的自动机。在OMG发布的UML2.0交互模型可视化语法的基础上,对UML2.0交互模型的语法和语义进行了抽象,描述了交互模型的基本语法,提出了一种形式化描述交互模型的B(?)chi自动机——交互自动机。在此基础上,本文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法,提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历,检测各状态的时态逻辑公式(CTL公式)的真值,以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。

论文目录

• 摘要
• Abstract
• 第一章 绪论
• 1.1 软件可靠性与形式化方法
• 1.2 UML模型形式化研究现状
• 1.3 本文的研究内容
• 1.4 本文的结构
• 第二章 模型检测技术
• 2.1 形式化方法
• 2.2 模型检测技术
• 2.3 时态逻辑和模型检测
• 第三章 UML交互模型
• 3.1 统一建模语言UML
• 3.1.1 UML2.0的结构
• 3.1.2 UML2.0的建模元素
• 3.1.3 UML的主要特点
• 3.2 UML交互模型在UML建模中的应用
• 第四章 形式化描述UML交互模型
• 4.1 UML交互模型的语法
• 4.1.1 UML的可视化描述
• 4.1.2 UML交互模型的抽象语法
• 4.2 用时态逻辑描述交互模型的性质
• 4.3 Büchi自动机
• 4.4 交互自动机
• 第五章 UML交互模型的模型检测方法
• 5.1 从UML2.0交互模型向交互自动机的转化
• 5.2 模型检测算法
• 5.2.1 基本算法
• 5.2.2 算法分析
• 5.3 UML交互模型检测算法的应用
• 第六章 总结与展望
• 6.1 总结
• 6.2 展望
• 参考文献
• 攻读学位期间的研究成果
• 致谢