基于Z规格的UML模型形式化转换及验证

张 杨，段 富

（太原理工大学 计算机科学与技术学院，山西 太原030024）

0 引 言

由于目前软件系统复杂性及规模度的与日俱增，开发的困难度与相应成本也在迅猛增加，因此，投入使用的软件产品存在错误和系统安全隐患的机率就随着软件规模成正向增长，通过人工方式排除效率低下且难度较大，而普通的软件测试方法也有测试疏漏和测试滞后性等诸多劣势［1，2］。鉴于上述现状，提出引入形式化技术的解决方案。

形式化方法为基于数学的方法，用以描述目标系统性质，通过严格的数学符号和相应法则，对系统的结构和行为进行高效简明的描述、分析、推理和演算，为系统属性的说明、开发及验证设计了框架，可有助于发现目标系统需求设计中的不一致性、不完备性等情况［3，4］。另一方面，半形式化语言与自然语言较为接近，通常使用图形方式进行抽象和建模，例如统一建模语言（UML）。因此，本文在UML模型中引入了形式化方法——Z规格说明，提出一种简明且高效的系统模型形式化转换及验证方式。

本文使用UML对目标系统建模，进而对得到的系统模型进行形式化描述和验证。Z提供了一种将应用系统描述为静态属性集合和动态谓词逻辑的表示法［5］。对所描述系统形式化结果的验证可通过谓词公式演算推导进而完成［6］。在从UML模型转化为Z规格说明的过程中，将用例图中的角色及其行为转化为Z中的集合和函数，将状态图所具有的性质及操作转化为相应状态和操作模式。当UML模型转化为Z规格说明结束时，通过Z规格说明定理证明器Z／EVES验证转化后得到的相应系统模型是否符合系统所需要满足的性质。

1 UML

UML是一种定义简明、表达直接、功能也较为全面且适用性强的建模语言，目前已经成为软件建模常规标准。视图类型多样是其最大的特点，使得UML可以从多方面为目标系统进行描述。

1.1 用例图

用例图是UML中用来描述描述外部执行者所理解的系统功能，显示系统中的用例与角色，及其相互关系，用于需求分析阶段，有利于理解系统的功能行为，帮助导出详细需求，是用户和开发者关于需求规格达成共识的体现。本文以电梯系统为例进行仿真，图1为一个电梯的UML用例图。

图1 电梯用例图

1.2 状态图

状态图的作用是对一个反应式对象的生存周期状态进行建模。一个状态图就是该反应式对象上的状态机。UML状态图具有以下主要元素：①状态名；②入口动作；③动作；④状态间转换：转换需要满足一定条件并且传递相应参数，形如name（parma）［guard］／action＿list，name是转换名，parma是所传递参数，guard是执行时所需要的条件，action＿list为转换执行时的动作列表。

2 形式化验证方法及Z

形式验证主要分以下三部分进行验证：

（1）初始状态存在验证

初始状态是存在于状态空间中的状态，也是对象的初态。在Z规格说明中，通常用Init作为模式名来表示。在得到完备的形式化规格说明之后，须验证其初始状态的存在性，即存在于状态空间［7］。有表达式为：｜－ -State＇·∧InitState。State’表示系统初始状态，InitState用来初始化，该定理的含义为存在一个State’系统状态满足InitState初始化操作模式的谓词，通过定理展开可以推导出结论。

（2）前置条件验证

对某操作模式，其前置条件即精确条件：在此条件下，给定的操作可用。前置条件标识符记作Pre，只限于描述操作模式，运算的结果为一个模式，称为条件模式。设OP是个模式，则可定义PreOP为：-State＇；Out！·OP。

这里State是系统的抽象状态，OP为该状态定义的操作模式，Outs！是OP的输出变量声明的集合。根据Z规格说明前置条件的求法：从表述操作模式的说明中删去后状态变量及输出变量，将谓词部分的此种变量使用存在量词进行量化。

在书写完形式规格说明后，需求出操作的前置条件，用以检验该操作前置条件是否满足需求规格。

（3）性质验证

证明初始化定理及化简前置条件是可对任意基于状态的规格说明进行的标准检查［8］。对一个特定的规格说明，有所希望的相应性质需要证明。这些性质可以是按非形式的需求所要求的。在Z中往往以定理的形式给出：OP｜Input｜－State。

OP为当前操作模式，Input为输入变量，根据OP模式中的说明部分和谓词部分，可以证明State不变，即可证明，在后面的例子中会加以具体阐述。

Z语言是基于集合论与一阶谓词逻辑的形式规格说明语言［9］。鉴于使用严谨的数学语言，可得到简洁、无二义性且可以进行逻辑验证的规格说明，故满足检测目标系统的可行性目的。

Z／EVES是一个用来检测Z规格说明的Z设计辅助工具。在一个规范性描述中，检测其能否符合所对应满足的系统属性是检查其错误最高效的方式［10］。Z／EVES可以检测Z规格说明所描述的句法和语义的正确性，然后根据谓词演算对所定义的集合和谓词公式进行有穷推导或者归约，以达到验证的目的。

3 UML到Z的转换

通过Z规格说明转换UML模型的具体流程如图2所示。

图2 UML模型转化为Z规格说明的流程

该方案从需求分析阶段开始，先定义用例，然后细化得到用例图，根据静态属性和动态行为的分类，分别构造用例图和状态图。将用例图抽象形式化描述为Z中的基本类型、幂集类型和对象声明，将状态图形式化描述为Z中的模式类型。将以上两部分整合为完备的Z规格说明，进而用Z／EVES进行形式化验证后，得到正确的Z规格说明，进而对系统性质进行可行性验证，从而得到该方案的可行性结论。

3.1 用例图的转化

用例图中有2类属性需形式化转化。角色和角色直接的关联或行为，通过转化可以得到UML模型相应Z规格说明的状态模式或不变式。

（1）角色

用Z语言将角色的类型或属性描述为基本类型或者幂集类型的集合，各集合元素都代表该类集合所满足的属性，而该属性则使用一阶谓词逻辑加以描述和限制。例如在图1中，电梯用户有 “maxsize”属性，电梯有 “maxfloor”，“state”和 “flag”这3个属性，在声明 “maxsize”属性时，由于Z规格说明不具有面向对象规格说明Object－Z所具有类之间的继承方式，故引入Z中的构造类型，声明作为一个电梯用户数量的给定集合类型

其中分别将电梯和电梯用户上述4个属性作如下形式化描述，如图3所示。

图3 定义变量声明

从而得到相应的状态模式如图4所示。

图4 状态模式

（2）角色行为

将角色行为转化Z中的函数关系。例如假设在电梯用户和电梯之间的关联为 “request”，在声明时，由于电梯系统存在运行状态及乘客人数的改变，所以通过自定义函数加以形式化描述。首先需要自定义取最大及最小值的函数maximum和minimum，如图5所示。

图5 取最值函数

其次定义电梯上升或下降一层所用到的函数add，dec，如图6所示。

图6 加减函数add，dec

最后定义计算函数cal，用以形式化描述电梯3种运行状态，如图7所示。

图7 计算函数cal

3.2 状态图的转化

UML中使用状态图、时序图等对系统模型的动态属性进行描述，而在Z规格说明中使用模式进行系统状态的描述。具体步骤如下：

（1）将每个状态定义为一个Z规格说明状态模式，相应的属性名及相应参数和UML模型相一致。

（2）通过前置条件描述进行如上转换时所需满足的约束条件。

（3）上述状态迁移时转换的入口动作以操作模式给出。

（4）若各状态已转换为Z规格说明，进行步骤 （5），反之进行步骤 （1）。

（5）将所有定义的状态模式和相应的操作模式与需求规格相比较，得到完整的操作模式。

假设图1中的电梯模型具有如下几类操作：外部上行请求操作 （OutUpRequest），外部下行请求操作 （Out－DownRequest），这两种操作等效于外部申请操作

此时即实现了状态图与用例图的功能等价对应。

根据内外部请求得到的电梯运行状态up＿run及down＿run，该模型的状态图如图8所示。

图8 电梯模型状态

根据如上状态图所示，按照状态图转化步骤，即可得到UML模型的初始化模式及各类操作模式。

以申请操作为例，若乘客在外面，属于外部请求，反之则是内部请求。内外请求之后，所到楼层数并入相对应的向上请求集合（upset）或者向下请求集合（downset）。需要注意，外部请求输入为一个序偶 （A＊ ｛－1，1｝），由所在楼层与向上或向下标识符构成，而内部请求仅在电梯内部，按所需要的层数按键，不涉及向上或者向下。

外部请求操作：外部向上申请操作（OutUpRequest）和外部向下申请操作（OutDownRequest）。

如图9和图10所示。

乘客在电梯外部的申请操作外部向下和向上申请的复合，因此有

Out Request＝ OutUpRequest ∨ OutDownRequest。

内申请操作：在电梯内部按键申请，如图11所示。

图11 内部申请操作

综上所述，得到完整的申请操作模式：Request＝InRequest ∨ Out Request。

4 形式化验证

在上一节中，已得到电梯系统UML模型，并根据相应步骤将其转换为Z规格说明的状态模式和相应的操作模式。在本节中需要验证该形式规格说明是否满足需求规格，可按第3节中的步骤检验。

4.1 初始状态验证

为了验证初始状态存在性，只需验证如下定理成立：

针对电梯实例，根据点规则 （one－point rule）化简有：

由状态变量和给定类型有：

即有结论true，故初始状态存在。

4.2 前置条件验证

验证前置条件时，得到相应的操作前置条件是必要的，然后和需求规格相比较，相符则形式化合理，否则不满足规格要求。

对于外部申请操作，按照第3节中介绍的Z规格前置条件求法，再按照点规则（One－point－rule）其谓词部分化简后可得：

对于前置条件PreOutRequest，有两种情况，即有

对于第一种情况前置条件表明，当电梯运行静止或向上运行 （tag＝static∨tag＝up），外部按键向上（ran（s？）＝1）和电梯当前位于按键楼层（dom（s？）＝story），且电梯门已关闭状态（door＝close），申请成功。其满足电梯的一般性要求。

当第二种情况时，前置条件说明电梯向上运行（tag＝up），外部按键所在的楼层与当前电梯所处楼层至少要相差一层（dom（s？）－story＞0），考虑电梯运行存在惯性，此时楼层的外部按键请求不会使电梯停止，按键请求向上时（ran（s？）＝1），申请成功。这符合设计要求。

对于其他操作的前置条件，证明类似，在此不作赘述。

4.3 UML模型的性质证明

根据第3节中的规格性质验证步骤，将推理得到的性质与相应需求规格比较，验证能否满足相应性质。此节只检验电梯进出乘客操作性质，其他类似。

对于Add＿Dec＿Man，根据OP｜Input｜－State证明方式，有：

表明操作Add＿Dec＿Man，若目前电梯是打开状态（door＝open），电梯里原有人数等于出去人数与进来人数进行线性求和，要求不超过电梯最大载客量maxsize，即（number＋n1？－n2！＜＝maxsize），此属于合法操作。进行该操作后，电梯现载人数等于曾经载客人数与出去人数、进入人数进行线性求和，即满足如下形式化描述（number＇＝number＋n1？－n2！），且电梯门关闭 （door＇＝close）。

5 结束语

本文提出了一种基于Z规格说明的UML模型检测方法，从初始状态的存在性，功能需求定义的准确性及各类型操作引发系统变化的状态转移进行检验，并将一个电梯系统UML实例转换为相应的Z规格说明，并给出了相应的形式化转换步骤和验证过程。虽然对简单的过程化系统而言，Z语言描述较为精确，但是随着面向对象技术的普遍应用，在形式化描述中添加面向对象技术应该是接下来迫切解决的问题，目前，Object－Z已经被提出以解决这个问题，该规格说明包括类的定义，通过谓词合取的方式继承以实现类之间多态、继承等操作。另外，Z规格还缺乏相应辅助设计工具，甚至是模型自动生成工具，这些将成为日后重点研究的内容。

：

［1］Freitas L，Woodcock J，ZHANG D Y.Verifying the CICS file control API with Z／Eves：An experiment in the verified software repository［J］.Science of Computer Programming，2009，74 （4）：197－218.

［2］Briaisa S，Nestmannb U.A formal semantics for protocol narrations［J］.Theoretical Computer Science，2007，389 （3）：484－511.

［3］Booch G，Rumbaugh J，Jacobson I.The unified modeling language user guide ［M］.2nd ed.Beijing：Machine Press，2006.

［4］Hasan O，Tahar S.Verification of probabilistic properties in the HOL theorem prover ［J］.Integrated Formal Methods，Springer，Berlin，2007，132 （8）：333－352.

［5］Zafar N A，Khan S A，Kamran B.Formal procedure of deriving language from context－free grammar ［C］／／International Conference on Intelligence and Information Technology，2010：533－536.

［6］Idani A，Ledru Y.Dynamic graphical UML views from formal B specifications ［J］.Information and Software Technology，2005，3 （8）：154－168.

［7］Zafar N A，Kamran B.Formal construction of possible operators on context－free grammar ［J］.International Conference on Intelligence and Information Technology，2010，52 （7）：223－243.

［8］Raj A，Prabhakar T V，Hendryx S.Transformation of SBVR business design to UML models ［C］／／India：Proceedings of the First India Software Engineering Conference，2008：112－124.

［9］Albert M，Gómez C，Cabot J，et al.Automatic generation of basic behavior schemas from UML class diagrams ［J］.Software and Systems Modeling，2010，9 （1）：47－67.

［10］Lima V，Talhi C，Mouheb D.Formal verification and validation of UML2.0sequence diagrams using source and destination of messages［J］.Electronic Notes in Theoretical Computer Science，2009 （254）：143－160.