基于Z規(guī)格的UML模型形式化轉(zhuǎn)換及驗(yàn)證

張 楊，段 富

（太原理工大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，山西 太原030024）

0 引 言

由于目前軟件系統(tǒng)復(fù)雜性及規(guī)模度的與日俱增，開(kāi)發(fā)的困難度與相應(yīng)成本也在迅猛增加，因此，投入使用的軟件產(chǎn)品存在錯(cuò)誤和系統(tǒng)安全隱患的機(jī)率就隨著軟件規(guī)模成正向增長(zhǎng)，通過(guò)人工方式排除效率低下且難度較大，而普通的軟件測(cè)試方法也有測(cè)試疏漏和測(cè)試滯后性等諸多劣勢(shì)［1，2］。鑒于上述現(xiàn)狀，提出引入形式化技術(shù)的解決方案。

形式化方法為基于數(shù)學(xué)的方法，用以描述目標(biāo)系統(tǒng)性質(zhì)，通過(guò)嚴(yán)格的數(shù)學(xué)符號(hào)和相應(yīng)法則，對(duì)系統(tǒng)的結(jié)構(gòu)和行為進(jìn)行高效簡(jiǎn)明的描述、分析、推理和演算，為系統(tǒng)屬性的說(shuō)明、開(kāi)發(fā)及驗(yàn)證設(shè)計(jì)了框架，可有助于發(fā)現(xiàn)目標(biāo)系統(tǒng)需求設(shè)計(jì)中的不一致性、不完備性等情況［3，4］。另一方面，半形式化語(yǔ)言與自然語(yǔ)言較為接近，通常使用圖形方式進(jìn)行抽象和建模，例如統(tǒng)一建模語(yǔ)言（UML）。因此，本文在UML模型中引入了形式化方法——Z規(guī)格說(shuō)明，提出一種簡(jiǎn)明且高效的系統(tǒng)模型形式化轉(zhuǎn)換及驗(yàn)證方式。

本文使用UML對(duì)目標(biāo)系統(tǒng)建模，進(jìn)而對(duì)得到的系統(tǒng)模型進(jìn)行形式化描述和驗(yàn)證。Z提供了一種將應(yīng)用系統(tǒng)描述為靜態(tài)屬性集合和動(dòng)態(tài)謂詞邏輯的表示法［5］。對(duì)所描述系統(tǒng)形式化結(jié)果的驗(yàn)證可通過(guò)謂詞公式演算推導(dǎo)進(jìn)而完成［6］。在從UML模型轉(zhuǎn)化為Z規(guī)格說(shuō)明的過(guò)程中，將用例圖中的角色及其行為轉(zhuǎn)化為Z中的集合和函數(shù)，將狀態(tài)圖所具有的性質(zhì)及操作轉(zhuǎn)化為相應(yīng)狀態(tài)和操作模式。當(dāng)UML模型轉(zhuǎn)化為Z規(guī)格說(shuō)明結(jié)束時(shí)，通過(guò)Z規(guī)格說(shuō)明定理證明器Z／EVES驗(yàn)證轉(zhuǎn)化后得到的相應(yīng)系統(tǒng)模型是否符合系統(tǒng)所需要滿(mǎn)足的性質(zhì)。

1 UML

UML是一種定義簡(jiǎn)明、表達(dá)直接、功能也較為全面且適用性強(qiáng)的建模語(yǔ)言，目前已經(jīng)成為軟件建模常規(guī)標(biāo)準(zhǔn)。視圖類(lèi)型多樣是其最大的特點(diǎn)，使得UML可以從多方面為目標(biāo)系統(tǒng)進(jìn)行描述。

1.1 用例圖

用例圖是UML中用來(lái)描述描述外部執(zhí)行者所理解的系統(tǒng)功能，顯示系統(tǒng)中的用例與角色，及其相互關(guān)系，用于需求分析階段，有利于理解系統(tǒng)的功能行為，幫助導(dǎo)出詳細(xì)需求，是用戶(hù)和開(kāi)發(fā)者關(guān)于需求規(guī)格達(dá)成共識(shí)的體現(xiàn)。本文以電梯系統(tǒng)為例進(jìn)行仿真，圖1為一個(gè)電梯的UML用例圖。

圖1 電梯用例圖

1.2 狀態(tài)圖

狀態(tài)圖的作用是對(duì)一個(gè)反應(yīng)式對(duì)象的生存周期狀態(tài)進(jìn)行建模。一個(gè)狀態(tài)圖就是該反應(yīng)式對(duì)象上的狀態(tài)機(jī)。UML狀態(tài)圖具有以下主要元素：①狀態(tài)名；②入口動(dòng)作；③動(dòng)作；④狀態(tài)間轉(zhuǎn)換：轉(zhuǎn)換需要滿(mǎn)足一定條件并且傳遞相應(yīng)參數(shù)，形如name（parma）［guard］／action＿list，name是轉(zhuǎn)換名，parma是所傳遞參數(shù)，guard是執(zhí)行時(shí)所需要的條件，action＿list為轉(zhuǎn)換執(zhí)行時(shí)的動(dòng)作列表。

2 形式化驗(yàn)證方法及Z

形式驗(yàn)證主要分以下三部分進(jìn)行驗(yàn)證：

（1）初始狀態(tài)存在驗(yàn)證

初始狀態(tài)是存在于狀態(tài)空間中的狀態(tài)，也是對(duì)象的初態(tài)。在Z規(guī)格說(shuō)明中，通常用Init作為模式名來(lái)表示。在得到完備的形式化規(guī)格說(shuō)明之后，須驗(yàn)證其初始狀態(tài)的存在性，即存在于狀態(tài)空間［7］。有表達(dá)式為：｜－ -State＇·∧InitState。State’表示系統(tǒng)初始狀態(tài)，InitState用來(lái)初始化，該定理的含義為存在一個(gè)State’系統(tǒng)狀態(tài)滿(mǎn)足InitState初始化操作模式的謂詞，通過(guò)定理展開(kāi)可以推導(dǎo)出結(jié)論。

（2）前置條件驗(yàn)證

對(duì)某操作模式，其前置條件即精確條件：在此條件下，給定的操作可用。前置條件標(biāo)識(shí)符記作Pre，只限于描述操作模式，運(yùn)算的結(jié)果為一個(gè)模式，稱(chēng)為條件模式。設(shè)OP是個(gè)模式，則可定義PreOP為：-State＇；Out！·OP。

這里State是系統(tǒng)的抽象狀態(tài)，OP為該狀態(tài)定義的操作模式，Outs！是OP的輸出變量聲明的集合。根據(jù)Z規(guī)格說(shuō)明前置條件的求法：從表述操作模式的說(shuō)明中刪去后狀態(tài)變量及輸出變量，將謂詞部分的此種變量使用存在量詞進(jìn)行量化。

在書(shū)寫(xiě)完形式規(guī)格說(shuō)明后，需求出操作的前置條件，用以檢驗(yàn)該操作前置條件是否滿(mǎn)足需求規(guī)格。

（3）性質(zhì)驗(yàn)證

證明初始化定理及化簡(jiǎn)前置條件是可對(duì)任意基于狀態(tài)的規(guī)格說(shuō)明進(jìn)行的標(biāo)準(zhǔn)檢查［8］。對(duì)一個(gè)特定的規(guī)格說(shuō)明，有所希望的相應(yīng)性質(zhì)需要證明。這些性質(zhì)可以是按非形式的需求所要求的。在Z中往往以定理的形式給出：OP｜Input｜－State。

OP為當(dāng)前操作模式，Input為輸入變量，根據(jù)OP模式中的說(shuō)明部分和謂詞部分，可以證明State不變，即可證明，在后面的例子中會(huì)加以具體闡述。

Z語(yǔ)言是基于集合論與一階謂詞邏輯的形式規(guī)格說(shuō)明語(yǔ)言［9］。鑒于使用嚴(yán)謹(jǐn)?shù)臄?shù)學(xué)語(yǔ)言，可得到簡(jiǎn)潔、無(wú)二義性且可以進(jìn)行邏輯驗(yàn)證的規(guī)格說(shuō)明，故滿(mǎn)足檢測(cè)目標(biāo)系統(tǒng)的可行性目的。

Z／EVES是一個(gè)用來(lái)檢測(cè)Z規(guī)格說(shuō)明的Z設(shè)計(jì)輔助工具。在一個(gè)規(guī)范性描述中，檢測(cè)其能否符合所對(duì)應(yīng)滿(mǎn)足的系統(tǒng)屬性是檢查其錯(cuò)誤最高效的方式［10］。Z／EVES可以檢測(cè)Z規(guī)格說(shuō)明所描述的句法和語(yǔ)義的正確性，然后根據(jù)謂詞演算對(duì)所定義的集合和謂詞公式進(jìn)行有窮推導(dǎo)或者歸約，以達(dá)到驗(yàn)證的目的。

3 UML到Z的轉(zhuǎn)換

通過(guò)Z規(guī)格說(shuō)明轉(zhuǎn)換UML模型的具體流程如圖2所示。

圖2 UML模型轉(zhuǎn)化為Z規(guī)格說(shuō)明的流程

該方案從需求分析階段開(kāi)始，先定義用例，然后細(xì)化得到用例圖，根據(jù)靜態(tài)屬性和動(dòng)態(tài)行為的分類(lèi)，分別構(gòu)造用例圖和狀態(tài)圖。將用例圖抽象形式化描述為Z中的基本類(lèi)型、冪集類(lèi)型和對(duì)象聲明，將狀態(tài)圖形式化描述為Z中的模式類(lèi)型。將以上兩部分整合為完備的Z規(guī)格說(shuō)明，進(jìn)而用Z／EVES進(jìn)行形式化驗(yàn)證后，得到正確的Z規(guī)格說(shuō)明，進(jìn)而對(duì)系統(tǒng)性質(zhì)進(jìn)行可行性驗(yàn)證，從而得到該方案的可行性結(jié)論。

3.1 用例圖的轉(zhuǎn)化

用例圖中有2類(lèi)屬性需形式化轉(zhuǎn)化。角色和角色直接的關(guān)聯(lián)或行為，通過(guò)轉(zhuǎn)化可以得到UML模型相應(yīng)Z規(guī)格說(shuō)明的狀態(tài)模式或不變式。

（1）角色

用Z語(yǔ)言將角色的類(lèi)型或?qū)傩悦枋鰹榛绢?lèi)型或者冪集類(lèi)型的集合，各集合元素都代表該類(lèi)集合所滿(mǎn)足的屬性，而該屬性則使用一階謂詞邏輯加以描述和限制。例如在圖1中，電梯用戶(hù)有 “maxsize”屬性，電梯有 “maxfloor”，“state”和 “flag”這3個(gè)屬性，在聲明 “maxsize”屬性時(shí)，由于Z規(guī)格說(shuō)明不具有面向?qū)ο笠?guī)格說(shuō)明Object－Z所具有類(lèi)之間的繼承方式，故引入Z中的構(gòu)造類(lèi)型，聲明作為一個(gè)電梯用戶(hù)數(shù)量的給定集合類(lèi)型

其中分別將電梯和電梯用戶(hù)上述4個(gè)屬性作如下形式化描述，如圖3所示。

圖3 定義變量聲明

從而得到相應(yīng)的狀態(tài)模式如圖4所示。

圖4 狀態(tài)模式

（2）角色行為

將角色行為轉(zhuǎn)化Z中的函數(shù)關(guān)系。例如假設(shè)在電梯用戶(hù)和電梯之間的關(guān)聯(lián)為 “request”，在聲明時(shí)，由于電梯系統(tǒng)存在運(yùn)行狀態(tài)及乘客人數(shù)的改變，所以通過(guò)自定義函數(shù)加以形式化描述。首先需要自定義取最大及最小值的函數(shù)maximum和minimum，如圖5所示。

圖5 取最值函數(shù)

其次定義電梯上升或下降一層所用到的函數(shù)add，dec，如圖6所示。

圖6 加減函數(shù)add，dec

最后定義計(jì)算函數(shù)cal，用以形式化描述電梯3種運(yùn)行狀態(tài)，如圖7所示。

圖7 計(jì)算函數(shù)cal

3.2 狀態(tài)圖的轉(zhuǎn)化

UML中使用狀態(tài)圖、時(shí)序圖等對(duì)系統(tǒng)模型的動(dòng)態(tài)屬性進(jìn)行描述，而在Z規(guī)格說(shuō)明中使用模式進(jìn)行系統(tǒng)狀態(tài)的描述。具體步驟如下：

（1）將每個(gè)狀態(tài)定義為一個(gè)Z規(guī)格說(shuō)明狀態(tài)模式，相應(yīng)的屬性名及相應(yīng)參數(shù)和UML模型相一致。

（2）通過(guò)前置條件描述進(jìn)行如上轉(zhuǎn)換時(shí)所需滿(mǎn)足的約束條件。

（3）上述狀態(tài)遷移時(shí)轉(zhuǎn)換的入口動(dòng)作以操作模式給出。

（4）若各狀態(tài)已轉(zhuǎn)換為Z規(guī)格說(shuō)明，進(jìn)行步驟 （5），反之進(jìn)行步驟 （1）。

（5）將所有定義的狀態(tài)模式和相應(yīng)的操作模式與需求規(guī)格相比較，得到完整的操作模式。

假設(shè)圖1中的電梯模型具有如下幾類(lèi)操作：外部上行請(qǐng)求操作 （OutUpRequest），外部下行請(qǐng)求操作 （Out－DownRequest），這兩種操作等效于外部申請(qǐng)操作

此時(shí)即實(shí)現(xiàn)了狀態(tài)圖與用例圖的功能等價(jià)對(duì)應(yīng)。

根據(jù)內(nèi)外部請(qǐng)求得到的電梯運(yùn)行狀態(tài)up＿run及down＿run，該模型的狀態(tài)圖如圖8所示。

圖8 電梯模型狀態(tài)

根據(jù)如上狀態(tài)圖所示，按照狀態(tài)圖轉(zhuǎn)化步驟，即可得到UML模型的初始化模式及各類(lèi)操作模式。

以申請(qǐng)操作為例，若乘客在外面，屬于外部請(qǐng)求，反之則是內(nèi)部請(qǐng)求。內(nèi)外請(qǐng)求之后，所到樓層數(shù)并入相對(duì)應(yīng)的向上請(qǐng)求集合（upset）或者向下請(qǐng)求集合（downset）。需要注意，外部請(qǐng)求輸入為一個(gè)序偶 （A＊ ｛－1，1｝），由所在樓層與向上或向下標(biāo)識(shí)符構(gòu)成，而內(nèi)部請(qǐng)求僅在電梯內(nèi)部，按所需要的層數(shù)按鍵，不涉及向上或者向下。

外部請(qǐng)求操作：外部向上申請(qǐng)操作（OutUpRequest）和外部向下申請(qǐng)操作（OutDownRequest）。

如圖9和圖10所示。

乘客在電梯外部的申請(qǐng)操作外部向下和向上申請(qǐng)的復(fù)合，因此有

Out Request＝ OutUpRequest ∨ OutDownRequest。

內(nèi)申請(qǐng)操作：在電梯內(nèi)部按鍵申請(qǐng)，如圖11所示。

圖11 內(nèi)部申請(qǐng)操作

綜上所述，得到完整的申請(qǐng)操作模式：Request＝InRequest ∨ Out Request。

4 形式化驗(yàn)證

在上一節(jié)中，已得到電梯系統(tǒng)UML模型，并根據(jù)相應(yīng)步驟將其轉(zhuǎn)換為Z規(guī)格說(shuō)明的狀態(tài)模式和相應(yīng)的操作模式。在本節(jié)中需要驗(yàn)證該形式規(guī)格說(shuō)明是否滿(mǎn)足需求規(guī)格，可按第3節(jié)中的步驟檢驗(yàn)。

4.1 初始狀態(tài)驗(yàn)證

為了驗(yàn)證初始狀態(tài)存在性，只需驗(yàn)證如下定理成立：

針對(duì)電梯實(shí)例，根據(jù)點(diǎn)規(guī)則 （one－point rule）化簡(jiǎn)有：

由狀態(tài)變量和給定類(lèi)型有：

即有結(jié)論true，故初始狀態(tài)存在。

4.2 前置條件驗(yàn)證

驗(yàn)證前置條件時(shí)，得到相應(yīng)的操作前置條件是必要的，然后和需求規(guī)格相比較，相符則形式化合理，否則不滿(mǎn)足規(guī)格要求。

對(duì)于外部申請(qǐng)操作，按照第3節(jié)中介紹的Z規(guī)格前置條件求法，再按照點(diǎn)規(guī)則（One－point－rule）其謂詞部分化簡(jiǎn)后可得：

對(duì)于前置條件PreOutRequest，有兩種情況，即有

對(duì)于第一種情況前置條件表明，當(dāng)電梯運(yùn)行靜止或向上運(yùn)行 （tag＝static∨tag＝up），外部按鍵向上（ran（s？）＝1）和電梯當(dāng)前位于按鍵樓層（dom（s？）＝story），且電梯門(mén)已關(guān)閉狀態(tài)（door＝close），申請(qǐng)成功。其滿(mǎn)足電梯的一般性要求。

當(dāng)?shù)诙N情況時(shí)，前置條件說(shuō)明電梯向上運(yùn)行（tag＝up），外部按鍵所在的樓層與當(dāng)前電梯所處樓層至少要相差一層（dom（s？）－story＞0），考慮電梯運(yùn)行存在慣性，此時(shí)樓層的外部按鍵請(qǐng)求不會(huì)使電梯停止，按鍵請(qǐng)求向上時(shí)（ran（s？）＝1），申請(qǐng)成功。這符合設(shè)計(jì)要求。

對(duì)于其他操作的前置條件，證明類(lèi)似，在此不作贅述。

4.3 UML模型的性質(zhì)證明

根據(jù)第3節(jié)中的規(guī)格性質(zhì)驗(yàn)證步驟，將推理得到的性質(zhì)與相應(yīng)需求規(guī)格比較，驗(yàn)證能否滿(mǎn)足相應(yīng)性質(zhì)。此節(jié)只檢驗(yàn)電梯進(jìn)出乘客操作性質(zhì)，其他類(lèi)似。

對(duì)于Add＿Dec＿M(jìn)an，根據(jù)OP｜Input｜－State證明方式，有：

表明操作Add＿Dec＿M(jìn)an，若目前電梯是打開(kāi)狀態(tài)（door＝open），電梯里原有人數(shù)等于出去人數(shù)與進(jìn)來(lái)人數(shù)進(jìn)行線性求和，要求不超過(guò)電梯最大載客量maxsize，即（number＋n1？－n2?。迹絤axsize），此屬于合法操作。進(jìn)行該操作后，電梯現(xiàn)載人數(shù)等于曾經(jīng)載客人數(shù)與出去人數(shù)、進(jìn)入人數(shù)進(jìn)行線性求和，即滿(mǎn)足如下形式化描述（number＇＝number＋n1？－n2?。?，且電梯門(mén)關(guān)閉 （door＇＝close）。

5 結(jié)束語(yǔ)

本文提出了一種基于Z規(guī)格說(shuō)明的UML模型檢測(cè)方法，從初始狀態(tài)的存在性，功能需求定義的準(zhǔn)確性及各類(lèi)型操作引發(fā)系統(tǒng)變化的狀態(tài)轉(zhuǎn)移進(jìn)行檢驗(yàn)，并將一個(gè)電梯系統(tǒng)UML實(shí)例轉(zhuǎn)換為相應(yīng)的Z規(guī)格說(shuō)明，并給出了相應(yīng)的形式化轉(zhuǎn)換步驟和驗(yàn)證過(guò)程。雖然對(duì)簡(jiǎn)單的過(guò)程化系統(tǒng)而言，Z語(yǔ)言描述較為精確，但是隨著面向?qū)ο蠹夹g(shù)的普遍應(yīng)用，在形式化描述中添加面向?qū)ο蠹夹g(shù)應(yīng)該是接下來(lái)迫切解決的問(wèn)題，目前，Object－Z已經(jīng)被提出以解決這個(gè)問(wèn)題，該規(guī)格說(shuō)明包括類(lèi)的定義，通過(guò)謂詞合取的方式繼承以實(shí)現(xiàn)類(lèi)之間多態(tài)、繼承等操作。另外，Z規(guī)格還缺乏相應(yīng)輔助設(shè)計(jì)工具，甚至是模型自動(dòng)生成工具，這些將成為日后重點(diǎn)研究的內(nèi)容。

：

［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.