張 楊，段 富

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

0 引 言

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

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

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

1 UML

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

1.1 用例圖

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

圖1 電梯用例圖

1.2 狀態(tài)圖

狀態(tài)圖的作用是對一個(gè)反應(yīng)式對象的生存周期狀態(tài)進(jìn)行建模。一個(gè)狀態(tài)圖就是該反應(yīng)式對象上的狀態(tài)機(jī)。UML狀態(tài)圖具有以下主要元素：①狀態(tài)名；②入口動(dòng)作；③動(dòng)作；④狀態(tài)間轉(zhuǎn)換：轉(zhuǎ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)，也是對象的初態(tài)。在Z規(guī)格說明中，通常用Init作為模式名來表示。在得到完備的形式化規(guī)格說明之后，須驗(yàn)證其初始狀態(tài)的存在性，即存在于狀態(tài)空間［7］。有表達(dá)式為：｜－ -State＇·∧InitState。State’表示系統(tǒng)初始狀態(tài)，InitState用來初始化，該定理的含義為存在一個(gè)State’系統(tǒng)狀態(tài)滿足InitState初始化操作模式的謂詞，通過定理展開可以推導(dǎo)出結(jié)論。

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

（1）角色

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

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

圖3 定義變量聲明

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

圖4 狀態(tài)模式

（2）角色行為

將角色行為轉(zhuǎn)化Z中的函數(shù)關(guān)系。例如假設(shè)在電梯用戶和電梯之間的關(guān)聯(lián)為 “request”，在聲明時(shí)，由于電梯系統(tǒng)存在運(yùn)行狀態(tài)及乘客人數(shù)的改變，所以通過自定義函數(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í)序圖等對系統(tǒng)模型的動(dòng)態(tài)屬性進(jìn)行描述，而在Z規(guī)格說明中使用模式進(jìn)行系統(tǒng)狀態(tài)的描述。具體步驟如下：

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

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

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

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

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

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

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

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

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

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

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

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

如圖9和圖10所示。

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

Out Request＝ OutUpRequest ∨ OutDownRequest。

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

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

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

4 形式化驗(yàn)證

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

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

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

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

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

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

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

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

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

對于前置條件PreOutRequest，有兩種情況，即有

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

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

對于其他操作的前置條件，證明類似，在此不作贅述。

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

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

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

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

5 結(jié)束語

本文提出了一種基于Z規(guī)格說明的UML模型檢測方法，從初始狀態(tài)的存在性，功能需求定義的準(zhǔn)確性及各類型操作引發(fā)系統(tǒng)變化的狀態(tài)轉(zhuǎn)移進(jìn)行檢驗(yàn)，并將一個(gè)電梯系統(tǒng)UML實(shí)例轉(zhuǎn)換為相應(yīng)的Z規(guī)格說明，并給出了相應(yīng)的形式化轉(zhuǎn)換步驟和驗(yàn)證過程。雖然對簡單的過程化系統(tǒng)而言，Z語言描述較為精確，但是隨著面向?qū)ο蠹夹g(shù)的普遍應(yīng)用，在形式化描述中添加面向?qū)ο蠹夹g(shù)應(yīng)該是接下來迫切解決的問題，目前，Object－Z已經(jīng)被提出以解決這個(gè)問題，該規(guī)格說明包括類的定義，通過謂詞合取的方式繼承以實(shí)現(xiàn)類之間多態(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.