统一建模语言(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交互模型是否符合计算机软件系统应满足的性质及规范。