魏先民，張玉艷

（濰坊學(xué)院，山東 濰坊 261061）

1 引言

模型驅(qū)動開發(fā)（Model－DrivenDevelopment，MDD［1］）已成為軟件工程技術(shù)的研究熱點(diǎn)和發(fā)展趨勢，它通過提升抽象層次來應(yīng)對軟件開發(fā)的復(fù)雜性。行為描述及其精化是MDD研究中的一個關(guān)鍵問題，它需要考慮對象的一系列動作語義，包括動作觸發(fā)的條件，動作對系統(tǒng)的影響以及動作之間的順序、并發(fā)等時空關(guān)系，但長期以來并未形成統(tǒng)一而行之有效的方法［1－3］。軟件系統(tǒng)的正確性和完備性可以通過對生命周期中不同產(chǎn)品和過程的形式化來提升，以集合論和謂詞邏輯為基礎(chǔ)的形式化方法是行為建模的一種較為有效的思路，如Z、B［4］和VDM等。形式化方法可提供消除歧義和精確定義的作用，并可通過嚴(yán)格證明以盡早發(fā)現(xiàn)描述中的錯誤。

形式化的開發(fā)方法可以實(shí)現(xiàn)自頂向下、逐步精化的開發(fā)模式，但其描述規(guī)范冗長復(fù)雜，缺乏可理解性，而且也缺乏工程化方法的支持［5］。傳統(tǒng)的涉及精化的相關(guān)研究主要關(guān)注精化理論的構(gòu)建和精化一致性的定義與證明。目前已提出的一些解決方案還很不完善，其應(yīng)用領(lǐng)域也受到很大限制，主要應(yīng)用在一些安全攸關(guān)的關(guān)鍵領(lǐng)域［4］。因此將形式化方法集成到流行的軟件開發(fā)技術(shù)和設(shè)計過程中，也已成為當(dāng)前形式化方法研究的一個趨勢和熱點(diǎn)［5］。作為面向?qū)ο蠼?biāo)準(zhǔn)的UML缺乏行為語義視角的定義，帶來模型描述的含混性，使得UML的語義規(guī)范和建模概念的含義對MDD的有關(guān)活動，如代碼自動生成和形式化驗(yàn)證來說是不夠的［6］。以微軟［3］和IBM［1］為代表的業(yè)界認(rèn)為，MDD的高層模型描述還不夠完備、精確，缺乏可理解的行為語義描述，因而難以完備、正確地實(shí)現(xiàn)模型轉(zhuǎn)換和精化。因此使用形式化方法描述系統(tǒng)的行為語義，將其與UML等建模語言相結(jié)合，共同描述軟件系統(tǒng)，受到越來越多的關(guān)注［5］。如何用形式化方法對系統(tǒng)行為進(jìn)行形式化描述，提高形式化方法在精化過程中的自動化和工程化支持，成為一個亟待解決的問題。

本文根據(jù)形式化方法建模理論，將形式化規(guī)范用作一系列的描述規(guī)范，提出了一種結(jié)構(gòu)模型約束下的行為模型描述方法，可為系統(tǒng)高層模型的行為描述以及模型轉(zhuǎn)換和精化提供細(xì)粒度的支持，從而為模型驅(qū)動的軟件開發(fā)提供有力的支持。

2 行為模型描述

以基于UML的ASLP方法［7］作為應(yīng)用系統(tǒng)高層模型的描述方法，它包含體系結(jié)構(gòu)建模和構(gòu)件建模兩個層次，其中構(gòu)件模型以功能視圖、工作流視圖、靜態(tài)視圖、行為視圖和界面展示視圖來統(tǒng)一描述。使用ASLP方法可為Web應(yīng)用建立平臺無關(guān)的模型描述，但其行為視圖是以基于UML的協(xié)作圖為基礎(chǔ)的，不能對構(gòu)件模型元素的行為提供細(xì)粒度的精確描述。本文即針對此問題進(jìn)行研究，以期對模型驅(qū)動的軟件開發(fā)提供全面的支持。

系統(tǒng)的行為描述是以該系統(tǒng)的結(jié)構(gòu)模型為基礎(chǔ)的，結(jié)構(gòu)模型提供了行為描述所依賴的數(shù)據(jù)結(jié)構(gòu)和上下文環(huán)境。

定義1 結(jié)構(gòu)模型（Structure Model）。結(jié)構(gòu)模型是一個三元組SM＝（Mid，AS，MS，CS），其中：

（1）Mid為模型的惟一標(biāo)識；

（2）AS是代表模型屬性的變量集合；

（3）MS＝｛mi｜i≥1｝是由模型的操作方法構(gòu)成的集合；

（4）CS是表達(dá)操作約束的謂詞公式構(gòu)成的集合。

圖1展示了一個整數(shù)序列的模型描述，其中INT與NAT分別代表整數(shù)與自然數(shù)，定義了求序列長度、取元素、交換兩元素的位置等操作方法。方法中涉及的參數(shù)若為只讀變量，則在其后附加“？”符號，類似地，寫變量和讀寫變量分別用“！”和“？！”來處理。

圖1 Sort行為模型

定義2 行為描述（Behavior Description）。行為描述是一個四元組，Behavior＝（IDBH，Pre，OL，Post），其中：

（1）IDBH是行為的標(biāo)識，包括行為的名稱、參數(shù)和返回值；

（2）Pre是行為的前條件謂詞；

（3）OL是由一系列操作方法構(gòu)成的操作邏輯，在概念上它可以表示為OL＝m0；m1；…；mk，并且?i∈（0..k）·（mi∈MS）。MS是環(huán)境提供的操作方法構(gòu)成的集合；

（4）Post是行為的后條件謂詞。

定義3 行為模型（Behavior Model）。行為模型是一個七元組，BM＝（Bid，LS，DM，INIT，RULE，F(xiàn)IN，ACTIONS），其中：

（1）Bid是行為模型的標(biāo)識；

（2）LS是局部變量的集合，它包含輸入、輸出和輸入輸出變量，分別用“？”、“！”和“？！”來表示；

（3）SM＝（Mid，AS，MS，CS）是行為模型所依賴的結(jié)構(gòu)模型；

（4）INIT是初始化行為；

（5）RULE＝｛RULEj｜j≥1｝是一個行為集合，稱為規(guī)則行為（RuleBehavior）集合，其中的行為都是基于結(jié)構(gòu)模型中的操作方法集合MS的；

（6）FIN是終止行為；

（7）ACTIONS是一個行為邏輯，它是行為模型的核心，由規(guī)則集合RULE的元素組成，表達(dá)了這個行為模型如何從初始化后，經(jīng)過一系列的行為操作最終到達(dá)終止返回的狀態(tài)。

一個行為可能是初始化行為INIT，終止行為FIN或者一般行為RULEj，形式化表示為：INIT（＝只有INIT 的前條件謂詞和FIN的后條件謂詞才能涉及全局變量，而其他謂詞都只涉及局部狀態(tài)變量。當(dāng)行為模型發(fā)生作用時，首先執(zhí)行初始化操作，根據(jù)此時結(jié)構(gòu)模型的狀態(tài)值，生成初始的局部狀態(tài)LS0；經(jīng)過一步或者多步行為（ACTIONS）的操作，局部變量最終轉(zhuǎn)化為LSm，最終經(jīng)過FIN行為返回全局變量的值。注意，這里的ACTIONS有可能為null，ACTIONS為null的行為模型稱為純抽象行為模型（Pure Abstract Behavior Model）。ACTIONS不為null的行為模型稱為一般行為模型（GeneralBehaviorModel），ACTIONS中包含抽象行為的行為模型稱為抽象行為模型（Abstract Behavior Model）。純抽象行為模型是抽象行為模型的特殊情況。

圖2以升序排序?yàn)槔x了一個基于圖1的結(jié)構(gòu)模型Sequenc的純抽象行為模型Ascending＿Sort。

3 行為精化

行為模型的精化通過跡的精化來定義。

定義4 跡（Trace）。系統(tǒng)行為的一個跡σ是一個有限或者無限的狀態(tài)序列，其長度為其狀態(tài)變遷的個數(shù)（用函數(shù)length表示），并且每個變遷都由一個行為引發(fā)，即□i∈（0..length（σ）－1）·（?B∈Behavior·（σ（i）｜＝Bσ（i＋1）））。

圖2 Sequence結(jié)構(gòu)模型

定義5 跡精化（Trace Refinement）。跡的精化，即前條件的弱化、后條件的強(qiáng)化和非確定性的減少，形式化表示為函數(shù)關(guān)系集合rel（B）為行為B發(fā)生前后系統(tǒng)狀態(tài)的映射集合［4］。

定義6 純抽象模型的實(shí)例化（Instantiation of Pure Abstract Behavior Model）。純抽象行為模型AM被具體行為模型CM精化，當(dāng)且僅當(dāng)CM對應(yīng)的跡σCM是AM對應(yīng)的跡的集合的元素，即

定義7 一般行為模型的精化（General Behavior Model Refinement）。假設(shè)存在兩個一般行為模型AM和CM，AM被CM精化，當(dāng)且僅當(dāng)它們對應(yīng)的跡σAM和σCM存在精化關(guān)系，形式化表示為

定義8 行為模型的實(shí)現(xiàn)（Realization of Behavior Model）。假設(shè)有兩個行為模型AM和CM，并且它們存在精化關(guān)系，即，如果CM的行為邏輯ACTIONS中的行為都能夠找到相關(guān)的原子行為實(shí)現(xiàn)，并且不包含任何的不確定性，也就是說，不包含抽象行為和一般的選擇結(jié)構(gòu)。這種特殊的一般行為模型的精化稱作行為模型的實(shí)現(xiàn)，并且稱CM為實(shí)現(xiàn)模型（Implementation Model）。

純抽象行為模型來自系統(tǒng)需求，是行為精化層次的最高層，只能被其他行為模型精化而不能成為任何行為模型的精化模型；實(shí)現(xiàn)模型可以直接轉(zhuǎn)化為可執(zhí)行程序，是行為精化層次的最底層，只能是其他行為模型的精化模型而不能成為任何行為模型的抽象模型。一般地，行為模型的精化過程中，首先可以從需求中得到純抽象行為，經(jīng)過逐步的精化，可以得到一個較為容易實(shí)施實(shí)例化的純抽象行為；經(jīng)過純抽象模型的實(shí)例化，可以得到一個有行為邏輯ACTIONS的一般行為模型，再經(jīng)過精化和實(shí)例化最終得到實(shí)現(xiàn)模型。

由精化的定義可知，行為模型的精化實(shí)際上就是行為模型的跡的精化。如果已知抽象模型并且其INIT和FIN行為一定的情況下，行為邏輯ACTIONS的求解便成了精化的核心問題。

命題1 每個行為模型的行為邏輯ACTIONS都可以等價于一個復(fù)雜行為。

證明：假設(shè)行為模型BM的行為邏輯ACTIONS的前條件為Preactions，狀態(tài)S，Si和Sf滿足由前面的定義知道因此容易得出，pre（ACTIONS）□post（INIT）∧pre（FIN）□post（ACTIONS）。如果取P＝Postinit∧Q＝Prefin，那么ACTIONS等價于復(fù)雜行為Beh（＝｛P｝ACTIONS｛Q｝。也可以對純抽象行為模型加以改造：由于它的ACTIONS為空，可以將其定義為一個抽象行為那么根據(jù)上述分析可知，這個ACTIONS等價于抽象行為

由命題1可以將精化問題轉(zhuǎn)化為在前后條件謂詞一定的情況下行為邏輯的實(shí)現(xiàn)問題，也就是說，精化的目的是減少行為邏輯中的抽象行為和不確定性結(jié)構(gòu)，使得行為模型最終轉(zhuǎn)化為實(shí)現(xiàn)模型。由于不確定性結(jié)構(gòu)只有借助其他的條件和限制才能得到精化，因此抽象行為模型將成為研究的主要目標(biāo)。對此類問題有兩種方法，分別是自下而上的歸約方法和自上而下的搜索方法。

自下而上的歸約方法是一種從目標(biāo)（行為的后條件Q）出發(fā)，經(jīng)過規(guī)約操作最終得到假設(shè)（行為的前條件P）的方法。這種方法減少了大量的中間狀態(tài)和中間變量，從而縮小了搜索空間，減少了問題求解的復(fù)雜度；然而它解決的問題比較簡單，對于復(fù)雜的問題，它只能起到化簡的作用。搜索方法是一種從假設(shè)（行為的前條件P）出發(fā)，經(jīng)過搜索操作最終得到目標(biāo)（行為的后條件Q）的方法。這種方法會產(chǎn)生大量的中間狀態(tài)，從而產(chǎn)生巨大的搜索空間而變成不可解問題，故必須采取啟發(fā)式的搜索方法，根據(jù)簡單謂詞邏輯公式和規(guī)則行為的觸發(fā)關(guān)系進(jìn)行規(guī)約操作，從而尋找出行為模型的一個可能的跡。

在解決方法中，歸約主要是為了消除公式中的量詞（包括全稱量詞?和存在量詞?），從而把公式分解為多個簡單邏輯公式，達(dá)到問題分解以縮小搜索空間的目的；而搜索主要是將多個簡單邏輯公式表達(dá)的抽象行為轉(zhuǎn)化為包含行為邏輯的具體行為，從而達(dá)到精化的目的，這稱為抽象行為的實(shí)現(xiàn)（Realization of Abstract Behavior）。每一個抽象行為的實(shí)現(xiàn)，都意味著抽象行為的減少，對整個行為模型而言都是一次精化。當(dāng)所有的抽象行為和不確定性結(jié)構(gòu)都不存在時，意味著實(shí)現(xiàn)模型的生成。在每一步精化操作之前，即處理每一個抽象行為時，用戶都可以根據(jù)每個抽象行為的前后條件添加相應(yīng)的行為，以人工干預(yù)的方式促進(jìn)搜索的快速完成。但用戶干預(yù)又可能會帶來新的全稱量詞和存在量詞，因此一旦行為中出現(xiàn)了這些量詞，都必須首先進(jìn)行歸約以產(chǎn)生粒度更小的抽象行為，然后才能搜索以完成抽象行為的實(shí)現(xiàn)。

圖2所示的純抽象行為模型經(jīng)過一系列歸約、搜索后得到的精化結(jié)果如下所示：

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

這個結(jié)果還需要進(jìn)一步精化和優(yōu)化處理?？梢圆捎米詣臃治龌蛉斯し治龅姆绞匠橄蟪龈鱾€分支所滿足的謂詞條件，進(jìn)而消除不確定性，實(shí)現(xiàn)排序算法，最后利用系統(tǒng)轉(zhuǎn)換程序?qū)⑵滢D(zhuǎn)換為某種編程語言的程序代碼，如Java、C＋＋等。

4 結(jié)束語

軟件開發(fā)的模型化和自動化是軟件技術(shù)的發(fā)展趨勢，結(jié)構(gòu)模型約束下的系統(tǒng)行為描述及其精化也成為近年來軟件工程領(lǐng)域研究的重點(diǎn)之一。本文根據(jù)形式化方法建模理論，在結(jié)構(gòu)模型描述的基礎(chǔ)上，提出了一種行為模型的形式化定義和描述框架，并進(jìn)一步實(shí)現(xiàn)了從行為的抽象模型到實(shí)現(xiàn)模型的精化。通過使用結(jié)構(gòu)模型的操作方法定義行為，提高了方法的重用性，而且使得搜索的粒度更大，加快了搜索的速度。下一步的工作將把這一功能集成到支持MDA的建模工具中［7］，從而為系統(tǒng)高層模型的行為描述和轉(zhuǎn)換（精化）提供細(xì)粒度的支持。

［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］.計算機(jī)工程，2007，33（8）：71－73.