支持模型驱动开发的行为描述方法＊

魏先民，张玉艳

（潍坊学院，山东 潍坊 261061）

1 引言

模型驱动开发（Model－DrivenDevelopment，MDD［1］）已成为软件工程技术的研究热点和发展趋势，它通过提升抽象层次来应对软件开发的复杂性。行为描述及其精化是MDD研究中的一个关键问题，它需要考虑对象的一系列动作语义，包括动作触发的条件，动作对系统的影响以及动作之间的顺序、并发等时空关系，但长期以来并未形成统一而行之有效的方法［1－3］。软件系统的正确性和完备性可以通过对生命周期中不同产品和过程的形式化来提升，以集合论和谓词逻辑为基础的形式化方法是行为建模的一种较为有效的思路，如Z、B［4］和VDM等。形式化方法可提供消除歧义和精确定义的作用，并可通过严格证明以尽早发现描述中的错误。

形式化的开发方法可以实现自顶向下、逐步精化的开发模式，但其描述规范冗长复杂，缺乏可理解性，而且也缺乏工程化方法的支持［5］。传统的涉及精化的相关研究主要关注精化理论的构建和精化一致性的定义与证明。目前已提出的一些解决方案还很不完善，其应用领域也受到很大限制，主要应用在一些安全攸关的关键领域［4］。因此将形式化方法集成到流行的软件开发技术和设计过程中，也已成为当前形式化方法研究的一个趋势和热点［5］。作为面向对象建模标准的UML缺乏行为语义视角的定义，带来模型描述的含混性，使得UML的语义规范和建模概念的含义对MDD的有关活动，如代码自动生成和形式化验证来说是不够的［6］。以微软［3］和IBM［1］为代表的业界认为，MDD的高层模型描述还不够完备、精确，缺乏可理解的行为语义描述，因而难以完备、正确地实现模型转换和精化。因此使用形式化方法描述系统的行为语义，将其与UML等建模语言相结合，共同描述软件系统，受到越来越多的关注［5］。如何用形式化方法对系统行为进行形式化描述，提高形式化方法在精化过程中的自动化和工程化支持，成为一个亟待解决的问题。

本文根据形式化方法建模理论，将形式化规范用作一系列的描述规范，提出了一种结构模型约束下的行为模型描述方法，可为系统高层模型的行为描述以及模型转换和精化提供细粒度的支持，从而为模型驱动的软件开发提供有力的支持。

2 行为模型描述

以基于UML的ASLP方法［7］作为应用系统高层模型的描述方法，它包含体系结构建模和构件建模两个层次，其中构件模型以功能视图、工作流视图、静态视图、行为视图和界面展示视图来统一描述。使用ASLP方法可为Web应用建立平台无关的模型描述，但其行为视图是以基于UML的协作图为基础的，不能对构件模型元素的行为提供细粒度的精确描述。本文即针对此问题进行研究，以期对模型驱动的软件开发提供全面的支持。

系统的行为描述是以该系统的结构模型为基础的，结构模型提供了行为描述所依赖的数据结构和上下文环境。

定义1 结构模型（Structure Model）。结构模型是一个三元组SM＝（Mid，AS，MS，CS），其中：

（1）Mid为模型的惟一标识；

（2）AS是代表模型属性的变量集合；

（3）MS＝｛mi｜i≥1｝是由模型的操作方法构成的集合；

（4）CS是表达操作约束的谓词公式构成的集合。

图1展示了一个整数序列的模型描述，其中INT与NAT分别代表整数与自然数，定义了求序列长度、取元素、交换两元素的位置等操作方法。方法中涉及的参数若为只读变量，则在其后附加“？”符号，类似地，写变量和读写变量分别用“！”和“？！”来处理。

图1 Sort行为模型

定义2 行为描述（Behavior Description）。行为描述是一个四元组，Behavior＝（IDBH，Pre，OL，Post），其中：

（1）IDBH是行为的标识，包括行为的名称、参数和返回值；

（2）Pre是行为的前条件谓词；

（3）OL是由一系列操作方法构成的操作逻辑，在概念上它可以表示为OL＝m0；m1；…；mk，并且∀i∈（0..k）·（mi∈MS）。MS是环境提供的操作方法构成的集合；

（4）Post是行为的后条件谓词。

定义3 行为模型（Behavior Model）。行为模型是一个七元组，BM＝（Bid，LS，DM，INIT，RULE，FIN，ACTIONS），其中：

（1）Bid是行为模型的标识；

（2）LS是局部变量的集合，它包含输入、输出和输入输出变量，分别用“？”、“！”和“？！”来表示；

（3）SM＝（Mid，AS，MS，CS）是行为模型所依赖的结构模型；

（4）INIT是初始化行为；

（5）RULE＝｛RULEj｜j≥1｝是一个行为集合，称为规则行为（RuleBehavior）集合，其中的行为都是基于结构模型中的操作方法集合MS的；

（6）FIN是终止行为；

（7）ACTIONS是一个行为逻辑，它是行为模型的核心，由规则集合RULE的元素组成，表达了这个行为模型如何从初始化后，经过一系列的行为操作最终到达终止返回的状态。

一个行为可能是初始化行为INIT，终止行为FIN或者一般行为RULEj，形式化表示为：INIT（＝只有INIT 的前条件谓词和FIN的后条件谓词才能涉及全局变量，而其他谓词都只涉及局部状态变量。当行为模型发生作用时，首先执行初始化操作，根据此时结构模型的状态值，生成初始的局部状态LS0；经过一步或者多步行为（ACTIONS）的操作，局部变量最终转化为LSm，最终经过FIN行为返回全局变量的值。注意，这里的ACTIONS有可能为null，ACTIONS为null的行为模型称为纯抽象行为模型（Pure Abstract Behavior Model）。ACTIONS不为null的行为模型称为一般行为模型（GeneralBehaviorModel），ACTIONS中包含抽象行为的行为模型称为抽象行为模型（Abstract Behavior Model）。纯抽象行为模型是抽象行为模型的特殊情况。

图2以升序排序为例定义了一个基于图1的结构模型Sequenc的纯抽象行为模型Ascending＿Sort。

3 行为精化

行为模型的精化通过迹的精化来定义。

定义4 迹（Trace）。系统行为的一个迹σ是一个有限或者无限的状态序列，其长度为其状态变迁的个数（用函数length表示），并且每个变迁都由一个行为引发，即□i∈（0..length（σ）－1）·（∃B∈Behavior·（σ（i）｜＝Bσ（i＋1）））。

图2 Sequence结构模型

定义5 迹精化（Trace Refinement）。迹的精化，即前条件的弱化、后条件的强化和非确定性的减少，形式化表示为函数关系集合rel（B）为行为B发生前后系统状态的映射集合［4］。

定义6 纯抽象模型的实例化（Instantiation of Pure Abstract Behavior Model）。纯抽象行为模型AM被具体行为模型CM精化，当且仅当CM对应的迹σCM是AM对应的迹的集合的元素，即

定义7 一般行为模型的精化（General Behavior Model Refinement）。假设存在两个一般行为模型AM和CM，AM被CM精化，当且仅当它们对应的迹σAM和σCM存在精化关系，形式化表示为

定义8 行为模型的实现（Realization of Behavior Model）。假设有两个行为模型AM和CM，并且它们存在精化关系，即，如果CM的行为逻辑ACTIONS中的行为都能够找到相关的原子行为实现，并且不包含任何的不确定性，也就是说，不包含抽象行为和一般的选择结构。这种特殊的一般行为模型的精化称作行为模型的实现，并且称CM为实现模型（Implementation Model）。

纯抽象行为模型来自系统需求，是行为精化层次的最高层，只能被其他行为模型精化而不能成为任何行为模型的精化模型；实现模型可以直接转化为可执行程序，是行为精化层次的最底层，只能是其他行为模型的精化模型而不能成为任何行为模型的抽象模型。一般地，行为模型的精化过程中，首先可以从需求中得到纯抽象行为，经过逐步的精化，可以得到一个较为容易实施实例化的纯抽象行为；经过纯抽象模型的实例化，可以得到一个有行为逻辑ACTIONS的一般行为模型，再经过精化和实例化最终得到实现模型。

由精化的定义可知，行为模型的精化实际上就是行为模型的迹的精化。如果已知抽象模型并且其INIT和FIN行为一定的情况下，行为逻辑ACTIONS的求解便成了精化的核心问题。

命题1 每个行为模型的行为逻辑ACTIONS都可以等价于一个复杂行为。

证明：假设行为模型BM的行为逻辑ACTIONS的前条件为Preactions，状态S，Si和Sf满足由前面的定义知道因此容易得出，pre（ACTIONS）□post（INIT）∧pre（FIN）□post（ACTIONS）。如果取P＝Postinit∧Q＝Prefin，那么ACTIONS等价于复杂行为Beh（＝｛P｝ACTIONS｛Q｝。也可以对纯抽象行为模型加以改造：由于它的ACTIONS为空，可以将其定义为一个抽象行为那么根据上述分析可知，这个ACTIONS等价于抽象行为

由命题1可以将精化问题转化为在前后条件谓词一定的情况下行为逻辑的实现问题，也就是说，精化的目的是减少行为逻辑中的抽象行为和不确定性结构，使得行为模型最终转化为实现模型。由于不确定性结构只有借助其他的条件和限制才能得到精化，因此抽象行为模型将成为研究的主要目标。对此类问题有两种方法，分别是自下而上的归约方法和自上而下的搜索方法。

自下而上的归约方法是一种从目标（行为的后条件Q）出发，经过规约操作最终得到假设（行为的前条件P）的方法。这种方法减少了大量的中间状态和中间变量，从而缩小了搜索空间，减少了问题求解的复杂度；然而它解决的问题比较简单，对于复杂的问题，它只能起到化简的作用。搜索方法是一种从假设（行为的前条件P）出发，经过搜索操作最终得到目标（行为的后条件Q）的方法。这种方法会产生大量的中间状态，从而产生巨大的搜索空间而变成不可解问题，故必须采取启发式的搜索方法，根据简单谓词逻辑公式和规则行为的触发关系进行规约操作，从而寻找出行为模型的一个可能的迹。

在解决方法中，归约主要是为了消除公式中的量词（包括全称量词∀和存在量词∃），从而把公式分解为多个简单逻辑公式，达到问题分解以缩小搜索空间的目的；而搜索主要是将多个简单逻辑公式表达的抽象行为转化为包含行为逻辑的具体行为，从而达到精化的目的，这称为抽象行为的实现（Realization of Abstract Behavior）。每一个抽象行为的实现，都意味着抽象行为的减少，对整个行为模型而言都是一次精化。当所有的抽象行为和不确定性结构都不存在时，意味着实现模型的生成。在每一步精化操作之前，即处理每一个抽象行为时，用户都可以根据每个抽象行为的前后条件添加相应的行为，以人工干预的方式促进搜索的快速完成。但用户干预又可能会带来新的全称量词和存在量词，因此一旦行为中出现了这些量词，都必须首先进行归约以产生粒度更小的抽象行为，然后才能搜索以完成抽象行为的实现。

图2所示的纯抽象行为模型经过一系列归约、搜索后得到的精化结果如下所示：

foreachi∈（1..length（s？））do

foeachj∈（1..length（s？））do

i＞j→（get（s？，i？）≥get（s？，j？）→skip）□

（get（s？，i？）＜get（s？，j？）→swap（s？！，i？，j？））

od

od

这个结果还需要进一步精化和优化处理。可以采用自动分析或人工分析的方式抽象出各个分支所满足的谓词条件，进而消除不确定性，实现排序算法，最后利用系统转换程序将其转换为某种编程语言的程序代码，如Java、C＋＋等。

4 结束语

软件开发的模型化和自动化是软件技术的发展趋势，结构模型约束下的系统行为描述及其精化也成为近年来软件工程领域研究的重点之一。本文根据形式化方法建模理论，在结构模型描述的基础上，提出了一种行为模型的形式化定义和描述框架，并进一步实现了从行为的抽象模型到实现模型的精化。通过使用结构模型的操作方法定义行为，提高了方法的重用性，而且使得搜索的粒度更大，加快了搜索的速度。下一步的工作将把这一功能集成到支持MDA的建模工具中［7］，从而为系统高层模型的行为描述和转换（精化）提供细粒度的支持。

［1］Hailpern B，Tarr P.Model－driven development：The good，the bad，and the ugly［J］.IBM Systems Journal，2009，45（3）：451－461.

［2］Snook C，Butler M.UML－B：Formal modelling and design aided by UML［J］.ACM Transactions on Software Engineering and Methodology，2006，15（1）：92－122.

［3］Thomas D.MDA：Revenge of the modelers or UML utopia？［J］.IEEE Software，2004，21（3）：15－17.

［4］Abrial J R.The B－Book：Assigning Programs to Meanings［M］.Cambridge University Press，1996.

［5］Kim S K，Burger D，Carrington D.An MDA approach towards integrating formal and informal modeling languages［C］／／Fitzgerald J，Hayes I，TarleckiA.Lecture notes in computer science.Heidelberg Germany：Springer，2005，3582：448－464.

［6］Philippi S.Automatic code generation from high level petri nets for model driven systems engineering［J］.Journal of Systems and Software，2010，79（10）：1444－1455.

［7］侯金奎，万建成，张玉艳.一种支持 MDA的PIM 建模方法［J］.计算机工程，2007，33（8）：71－73.