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

摘要：该文详细介绍了统一建模语言和模型检测技术，在此基础上，该文研究了基于交互自动机和时态逻辑的UML交互模型性质检测方法，提出了模型检测所需的Marking算法。该算法通过对交互自动机全部状态的遍历，检测各状态的时态逻辑公式（CTL公式）的真值，以判断用户设计的UML交互模型是否符合计算机软件系统应满足的性质及规范。

关键词：时态逻辑；UML交互模型；模型检测；自动机

中图分类号：TP311文献标识码：A文章编号：1009-3044(2008)34-1975-02

Study on UML Interactions Model Based on Temporal Logic

CHEN Chun-hua1, XIE Fang-wen2, YUE Zeng-gang3

(1.Registry, Liaocheng Vocationnal and Technical College, Liaocheng 252000, China; puter School, Liaocheng University, Liaocheng 252059, China; 3.Department of Student Affairs, LiaochengUniversity, Liaocheng 252059, China)

Abstract: The paper investigates the model checking method to verify the properties of UML interaction models with interactive automaton and the temporal logic, and presents the Marking algorithm for model checking. This algorithm judges whether the UML interaction models designed by users satisfies the property and the standard of the software system, by marking all the states of interactive automaton, and checking the value of the CTL formulas of each state.

Key words: temporal logic; UML Interactions; Model checking; automaton

1 前言

UML（Unified Modeling Language，统一建模语言）作为新一代面向对象建模语言得到了广泛的支持，已经成为事实上的工业标准[1]。作为一种可视化的建模语言，UML可以从多个视角从不同的侧重点描述系统的性质[2]。目前，UML形式化方法的两个主要思路是：一是对UML核心语法进行形式化，使得UML成为符合形式化规范的语言；另一种是转换法，利用形式化语言在不丢失或者少丢失信息的前提下对UML进行形式化[3]。

UML模型主要应用在软件生命周期的分析和设计阶段，在UML建模的过程中尽可能少的引入错误，对于软件的可靠性和正确性是重要的。而UML模型的形式化对于验证UML模型的正确性和其它性质也是有效的。国外一些研究机构很早就对UML模型的形式化进行研究，提出了很多技术和方法，但是国内在这方面的研究起步比较晚，研究的也比较少，还主要集中在对UML的形式化描述方面，涉及UML模型检测的并不多。

2 模型检测技术

模型检测(Model Checking)是最早由美国卡耐基梅隆大学的Clarke 等人提出的一种自动验证有限状态系统的形式化验证技术，它以穷尽搜索为基础，通过遍历系统模型的状态空间来检测系统模型是否满足给定的性质，该方法与系统或程序以及系统性质的表示有很大的关系[4]。模型检测技术有两种实现方法，一种是基于对系统状态空间的有穷搜索，另一种是基于自动机理论。在后一种方法中，模型和待检测属性都被转化为自动机的输入语言，并输入到自动机中，通过相应的模型检测算法得出检测结果，从而判定系统是否满足给定属性。

时态逻辑(Temporal Logics)，又称时序逻辑，是一种特殊的模态逻辑，也是一种描述系统中状态迁移序列的形式化方法。时态逻辑是模型检测的基础，用以描述并发系统的性质，不同的时态逻辑有其相应的时态逻辑算子及其对应的语义。

时态逻辑通常是按照时间是否被假设为一个线性或分支结构来进行分类。有一些学者提议用时态逻辑来推理计算机程序，而Pnueli第一次用时态逻辑来推理并发系统。他的方法是通过一组描述程序中单个语句行为的公理来证明程序的性质。该方法被Bochmann、Malachi和Owicki扩充到顺序电路中。由于是手工进行证明，该技术通常在实践中难以应用[8]。

Clarke和Emerson在80年代早期引入时态逻辑模型检测算法，使这类兵法系统的推理可以实现自动化，他们在文献[5]中提出了针对计算树逻辑(Computing Tree Logic，CTL)的算法，对于程序模型的大小和时态逻辑公式的长度都是多项式复杂度的。Queille和Sifakis同时也为CTL的一个子集给出了模型检测算法[6]，但他们没有分析算法的复杂性。

经过多年的实践证明，各类时态逻辑理论是非常有表达力的逻辑，为模型检测技术提供了强有力的帮助。

在普通的命题逻辑中增加时态逻辑算子，就演变成为时态逻辑。时态逻辑算子的定义如表1所示。

3 形式化描述UML交互模型

计算机软件系统设计模型中的UML2.0交互可以作为系统的一个观测哨，用来观测消息的交换及状态的变化。当系统发送、接收一个消息或者系统的一个对象成功终止时，UML2.0交互将会作出相应的反应；当系统的状态发生变化时，交互也将做出相应的移动。

为了对UML2.0交互模型进行有关性质的检测，首先应将UML2.0交互模型进行形式化的描述，使其转化为一种可以接受消息交换或系统状态变化的自动机。

UML作为一种可视化的面向对象建模语言，其语法是基于图形的。OMG在[7]中用可视化的方式给出了UML的抽象描述，如图1所示，UML交互模型是在BasicInteraction包和Fragments包中定义的[7]。

图2给出了BasicInteraction包中有关UML交互模型的定义。

交互(Interactions)是交互模型中最基本的元素之一，它是通过继承UML::CommonBehaviors::BasicBehaviors::Behavior而得到的。从交互的定义即可知道交互其实是一种行为，它是对象为完成某种任务而互相传递的消息序列。在一个交互中，对象可以被创建和析构，对象之间可以彼此查询、触发对方的操作或使用信号通知对方当前发生的事件。

图2中还给出了交互(Interactions)和交互片段(InteractionsFragment)之间的组合关系，一个或多个交互片段可以组合为交互。

■

图1 交互模型在UML模型中的依赖性图2 交互模型中的Interactions语法

4 UML交互模型的模型检测方法

计算机软件系统的模型检测方法主要有两类：一类是基于状态空间的显式枚举，该方法大多是在自动机理论框架下实现的；另一类是基于状态空间的隐式枚举，如symbolic方法等。本章主要采用基于自动机理论的方法针对UML2.0交互模型进行模型检测。

基于自动机理论框架的模型检测，主要是讨论有穷或无穷序列上的有限自动机，通过遍历有限自动机的所有状态和所有路径，以检测系统是否具备指定的性质。

针对CTL的模型检测算法最初是由Emerson，Clarke， Sistla[8]和Queille，Sifakis[6]等人提出的。这个基础算法在模型验证和模型检测领域得到了广泛的应用，尤其是在计算机硬件系统模型的验证和检测方面，主要是由于算法在模型每个部分检测的应用中，时间复杂性上呈现线性特征，一定程度的避免了状态爆炸。

CTL模型检测算法的基本部分是运行在自动机上的标记算法(Marking algorithm)[7]。标记算法首先引入一个CTL公式p，对于自动机A中的任意一个状态s和p的任意一个子公式f，标记在状态s中是否满足f，即s|=f 。如果s|=f ，则s.f赋值为true，否则，s.f赋值为false。

本文分别描述了UML2.0交互模型向交互自动机转化和针对交互自动机的模型检测算法，对文中描述的系统处理对象缓存的交互模型，也给出了交互模型的形式化时态逻辑语义：

■

其中，系统状态的性质可以用CTL公式描述为：

■

即初始时刻Client未获得对象，在交互的结束时刻Client应获得对象，且对象在Cache中。

下面，我们应用算法对交互自动机及上述时态逻辑性质进行模型检测，其中参数IA为交互自动机(以下记为IA56)，Start为CTL公式集合{■ Client.Get,Cache.In}，Final为CTL公式集合{Client.Get,Cache.In}

Start集合中有两个CTL公式，分别描述了系统应具备的两个性质，首先针对初始性质■ Client.Get对交互自动机的16个状态所包含的系统性质进行标记，调用Marking算法，其中参数IA为IA56，p为CTL公式■ Client.Get。由于p=■ Client.Get符合case分支的第二个分支，运行到算法的第7行：

■

接下来，递归调用Marking算法，其中参数IA为IA56，p为CTL公式Client.Get。此时，p为原子命题，符合case分支的第一个分支，运行到算法的第4行：

■ （下转第1996页）

（上接第1976页）

对于交互自动机IA56中的所有状态s，如果s的时态逻辑命题集合中包含Client.Get，那么s.Client.Get赋值为true；对于其他状态s，s.Client.Get赋值为false。这样，s_11.Client.Get为true，其他状态的Client.Get为false。

接下来，执行算法的第9行：

■

对于交互自动机IA56中的所有状态s，将s.■ Client.Get的赋值为s.Client.Get的相反值。这样，就完成了对系统性质■ Client.Get的Marking算法。同样地，可以对系统性质Cache.In调用Marking算法，也对交互自动机进行遍历。

下面，我们看交互自动机的接受状态s_11。s_11中的时态逻辑命题主要包括Client.Get和Cache.In。经过Marking(IA56,Client.Get)和Marking(IA56,Cache.In)两次遍历，可以得到

s_11.Client.Get=true;s_11.Cache.In=true.

调用算法中的4~10行的双重for循环，可以得到交互模型满足系统性质的结论。

5 结论

统一建模语言UML2.0以及成为目前计算机软件分析与设计领域内的通用建模语言，广泛的应用于各类计算机软件系统的建模过程。该文在自动机理论的框架内，采用时态逻辑的性质描述方法，提出了针对UML2.0交互模型的模型检测方法。

模型检测技术在计算机软件系统中的应用还有许多问题尚待解决，UML模型的检测更是一个新兴的研究领域。在交互自动机的设计中，还需要对触发交互的条件、门以及交互触发的系统动作进行深入的研究。在未来的研究中，应进一步深入完善交互模型的形式化描述和检测方法。

参考文献:

[1] Kobryn C.UML 2001: a Standardization Odyssey[J].Communications of the ACM,1999,42(10):29-37.

[2] 黄正宝,张广泉.一种基于时序逻辑的UML2.0形式化语义[J].计算机科学,2006,33(8):218-221.

[3] 周欣,魏生民.基于B语言的UML形式化方法[J].计算机工程,2004,30(12):62-64.

[4] 许维新,虞慧群.基于TCOZ的UML用例图的形式化模型[J].华东理工大学学报,2004,30(1):82-87.

[5] Clarke E M,Emerson E A,Sistla A P.Automatic verification of finite-state concurrent systems using temporal logic specifications[J].ACM Transactions on Programming Languages and Systems,1986,8(2):244-263.

[6] Clarke E M,Emerson E A.Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic[J].Lecture Notes in Computer Science,1981,131(5):52-71.

[7] Queille J P,Sifakis J.Specification and Verification of Concurrent Systems in CESAR[J].Lecture Notes in Computer Science, 1982,137(4):337-351.

[8] Bérard B,Bidoit M,Finkel A,et al.Systems and Software Verification: Model-Checking Techniques and Tools[M].Berlin:Springer,2001.