基于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?。迹絤axsize），此屬于合法操作。進行該操作后，電梯現載人數等于曾經載客人數與出去人數、進入人數進行線性求和，即滿足如下形式化描述（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.