SysML 狀態(tài)圖合理性驗證研究與實現(xiàn)

俞曉鋒，王立松

(南京航空航天大學 計算機科學與技術(shù)學院，江蘇 南京 210016)

SysML(Systems Modeling Language)［1］是UML 在系統(tǒng)工程應(yīng)用領(lǐng)域的延續(xù)和拓展。與其他建模語言一樣，SysML 是一種通用標準建模語言。

隨著應(yīng)用系統(tǒng)越發(fā)復(fù)雜，系統(tǒng)的任意環(huán)節(jié)均可能會影響到系統(tǒng)的整體運行。例如民航業(yè)務(wù)系統(tǒng)，作為一個巨大的系統(tǒng)，不能保證其對象在整個生命期內(nèi)均能安全穩(wěn)健運行，而一旦出現(xiàn)異常狀況會造成巨大的經(jīng)濟損失。用SysML 建?？沙橄蟊硎緫?yīng)用系統(tǒng)的對象，本文研究的對象是類模型中某個主動類的實例，通過驗證行為模型來模擬出對象在生命期內(nèi)的運行過程，用這種方式來演練其實現(xiàn)的每一個用例場景。SysML 狀態(tài)圖用于建立類對象在其生命期內(nèi)的行為模型，尤其是當對象具有依賴于狀態(tài)的行為。

SysML 和UML 一樣，為保持描述的清晰易懂，在給出自身語義說明的同時，采用半形式化的描述方法，使用自然語言表示約束和語義，力求實現(xiàn)形式化與易于理解之間的平衡。因此，SysML 本身缺乏分析和驗證的手段，針對這一問題，本文對SysML 狀態(tài)圖進行拓展，使用SCXML(State Chart XML)［2］作為SysML 狀態(tài)圖的形式化描述語言并引用動作規(guī)約語言［3］(Action Specification Language，ASL)描述狀態(tài)圖對象的行為動作。其中ASL 是WilKie 等人在2002 年提出的平臺無關(guān)動作描述語言，其提供了操作平臺無關(guān)模型元素的方法。通過使用SCXML 和ASL 可建立精確無歧義的行為模型，并在此基礎(chǔ)上進行分析驗證。

SysML 狀態(tài)圖的體系結(jié)構(gòu)驗證無需考慮業(yè)務(wù)需求的偏好，使用Kripke 結(jié)構(gòu)可表示對象的狀態(tài)空間。由于SCXML 可表示SysML 狀態(tài)圖體系結(jié)構(gòu)的所有信息，根據(jù)Kripke 結(jié)構(gòu)可方便構(gòu)造出SysML 狀態(tài)圖的對象狀態(tài)遷移圖，通過對象狀態(tài)遷移圖給出性能需求的形式化表示和驗證算法［4］。在業(yè)務(wù)需求驗證方面，主要考察對象在生命期內(nèi)的行為過程是否與用例時序圖一致，本文采用事件信號驅(qū)動機制來捕獲對象的行為軌跡。

1 SysML 狀態(tài)圖體系結(jié)構(gòu)驗證

1.1 SysML 狀態(tài)圖語義

為便于描述，本文在遵從對象管理組織SysML 規(guī)范［5］的前提下重新定義了一些狀態(tài)圖語義的形式化表示方式，包括順序自動機、層次自動機、單元以及層次自動機的操作語義。

驗證SysML 狀態(tài)圖的體系結(jié)構(gòu)，首先將狀態(tài)圖轉(zhuǎn)化為層次自動機(HA)，其由順序自動機(SA)組成。

定義2 HA=(F，E)，F(xiàn) 是有窮順序自動機集合;?SA1，SA2∈F，ΨSA1∩ΨSA2=Φ，E 是有窮事件集合。

HA 中的全局狀態(tài)由單元表示，一個單元既可以代表一個基本狀態(tài)又可代表一個復(fù)合狀態(tài)，每個復(fù)合狀態(tài)由某個簡單順序自動機的基本狀態(tài)組成。

在SysML 狀態(tài)圖中，每個狀態(tài)由單元和當前環(huán)境組成，環(huán)境包括事件環(huán)境和變量環(huán)境，對于事件環(huán)境E，ΘE 表示事件隊列的所有可能情況，對于變量環(huán)境V;ΘV 表示變量所有可能取值。下面用標記轉(zhuǎn)換系統(tǒng)(LTS)對HA 定義操作語義。

定義4 HA 的操作語義是一個LTS OP=(S，S0，→)，其中S=CellHA×ΘE×ΘV 是狀態(tài)集合，S0是初始狀態(tài)集合，→=S×S 是狀態(tài)遷移集合。

1.2 通過SCXML 構(gòu)造對象狀態(tài)遷移圖

Kripke 結(jié)構(gòu)是一個4 元組，K=(CellHA，→，L，Cell0)，其中，是初始單元的合集;(Cell1，Cell2)∈→表示存在從Cell1到Cell2的遷移，假設(shè)→中的遷移互不相同;L∶CellHA→2AP為每個單元標注一組原子命題。

本文采用鄰接表來實現(xiàn)Kripke 結(jié)構(gòu)，實例如圖1所示。

圖中Vs1，Vs2，Vs3，Vs4∈CellHA，所有鄰接于Vsi的頂點Sj鏈成一條單鏈表，其中Vsi，Sj∈CellHA，?i ∈{1，…，num}，此例中num 取4。

根據(jù)定義4，給出s∈S 的SCXML 表示，其中e1，…，en∈E，a1…，am∈V)。

圖1 用鄰接表表示Kripke 結(jié)構(gòu)的實例

從SCXML 可知SysML 狀態(tài)圖的操作語義，結(jié)合Kripke 結(jié)構(gòu)，便能構(gòu)造出對象狀態(tài)遷移圖G。G 是具有SysML 狀態(tài)圖操作語義的Kripke 結(jié)構(gòu)的抽象表示［10－11］。

生成對象狀態(tài)遷移圖G 的步驟如下:(1)初始化鄰接表。(2)從SCXML 中讀取Vsi∈CellHA和變量V 存放到鄰接表的頂點域里。(3)從SCXML 中讀取Vsi的遷移目標狀態(tài)存放到鄰接于Vsi的單鏈表里。(4)從SCXML 中讀取Vsi的事件E 存放到與Sji對應(yīng)的鏈接域里。(5)重復(fù)步驟(1)～步驟(3)直到讀取完SCXML 中所有的Vsi。(6)對象狀態(tài)遷移圖G 生成完成，算法結(jié)束。

1.3 性能需求驗證的標準

SysML 狀態(tài)圖是否滿足性能需求指主動類對象能否安全地運行完整個生命期［6－9］，即保證對象能夠安全地創(chuàng)建、銷毀并且在生命期內(nèi)不存在死鎖。根據(jù)這個要求，本文定義了G 的3 大安全性條件并給出了相關(guān)的推論和證明。

推論1 滿足條件1 和條件2 的狀態(tài)圖是符合狀態(tài)可達的，即狀態(tài)圖中任意一個狀態(tài)都是可達的。

條件3 tsi=(s1，s2，…，sj)∈{ts1，…，tsn}是對象的其中一條并發(fā)遷移序列，則ts1∩…∩tsi∩…∩tsn?{o}，其中o 為終止狀態(tài)。該條件表明對象收到銷毀信號時，不可能存在該對象產(chǎn)生的某個或多個子對象還未銷毀的情況，否則子對象會一直存在于系統(tǒng)中占用資源。保證了對象被安全銷毀。

在驗證性能需求時，使用G 的安全性作為正確性標準。

1.4 性能需求的驗證算法

本文定義了兩種異常狀態(tài)，分別取名為“奇跡”狀態(tài)和“黑洞”狀態(tài)。

定義5 “奇跡”狀態(tài)是一種只有遷移出，沒有遷移入的非初始狀態(tài)。對象處于這種狀態(tài)時說明它沒有被正確創(chuàng)建。

定義6 “黑洞”狀態(tài)是一種只有遷移入，沒有遷移出的非終止狀態(tài)。對象處于這種狀態(tài)說明它已經(jīng)陷入死鎖。

由推論1 可知，SysML 狀態(tài)圖不能存在“奇跡”和“黑洞”狀態(tài)，驗證算法:(1)遍歷G 的頂點域Vsi，判斷該頂點域的單鏈表是否為空，如果為空并且該頂點域中的狀態(tài)不是終止狀態(tài)，則存在“黑洞”狀態(tài)，標記異常，否則符合安全性的條件1。(2)遍歷G 的頂點域Vsi，如果該頂點域的單鏈表非空，則遍歷該單鏈表，并給單鏈表中的每個Sji標記上后繼標志。(3)在步驟(2)的基礎(chǔ)上重新遍歷頂點域Vsi，判斷頂點域中的狀態(tài)是否有后繼標志，如果沒有并且該狀態(tài)不是初始狀態(tài)，則存在“奇跡”狀態(tài)，標記異常，否則符合安全性的條件2。(4)如果終止狀態(tài)的前繼狀態(tài)只有1 個，則符合安全性的條件3，直接跳到步驟(8)，否則進行步驟(5)～步驟(7)。(5)遍歷G 的頂點域Vsi，判斷頂點域中的狀態(tài)類型，如果為FORK 偽狀態(tài)，則給該單鏈表中的每個Sji標記上活動標志，如果為JOIN 偽狀態(tài)，則清除頂點域中狀態(tài)的活動標記。(6)如果頂點域Vsi中的狀態(tài)具有活動標志，則給該單鏈表中的每個Sji標記上活動標志。(7)在步驟(5)和步驟(6)的基礎(chǔ)上重新遍歷G的頂點域Vsi，判斷頂點域中的狀態(tài)類型，如果為終止狀態(tài)并且具有活動標記，說明不符合安全性的條件3，標記異常，否則符合安全性的條件3。(8)如果條件1 ～條件3 都滿足，則該SysML 狀態(tài)圖的性能需求是合理的。

2 SysML 狀態(tài)圖業(yè)務(wù)需求驗證

2.1 業(yè)務(wù)需求驗證標準

一個用例從黑盒的、外部的角度描述了系統(tǒng)對象的一次生命過程。用它可推斷對象對請求或激勵做出何種響應(yīng)。全體用例和它們的相關(guān)場景，可以完全刻畫對象所需的功能性行為，使得絕大多數(shù)業(yè)務(wù)需求得以體現(xiàn)。用例時序圖是用戶希望系統(tǒng)所能產(chǎn)生的行為交互過程，它在建模過程中被用來當成系統(tǒng)的標準黑箱視圖。一個用例場景對應(yīng)一個用例時序圖。本文采用Moore 狀態(tài)機原型，在狀態(tài)圖模型描述某個主動類對象的行為過程中，當對象接收到外部激勵信號時所表現(xiàn)的行為由對象所在狀態(tài)的入口動作決定，它由ASL 進行描述，此時對象可能會在自導(dǎo)信號的作用下轉(zhuǎn)移到新的狀態(tài)也有可能停留在原狀態(tài)等待新的外部激勵，對象在這兩種情況下產(chǎn)生收發(fā)信號事件的序列。通過判斷信號事件序列是否符合預(yù)期定義的事件序列來驗證狀態(tài)圖的業(yè)務(wù)需求。

2.2 業(yè)務(wù)需求驗證設(shè)計方法

每個對象維持一個信號事件隊列，根據(jù)這個特點設(shè)計信號事件驅(qū)動機制來執(zhí)行狀態(tài)圖，設(shè)計的信號事件驅(qū)動結(jié)構(gòu)如圖2 所示。

圖2 信號事件驅(qū)動框架

事件消費類中的事件處理函數(shù)為狀態(tài)的入口動作，事件類中產(chǎn)生的信號包括外部信號事件和自導(dǎo)信號，狀態(tài)解析引擎將狀態(tài)圖轉(zhuǎn)換為由SCXML 和ASL表示的精確描述的PIM 代碼。如果狀態(tài)驗證沒有完成，整個驅(qū)動引擎將一直處于循環(huán)狀態(tài)，將驅(qū)動引擎生命期內(nèi)對象所產(chǎn)生的信號事件序列與預(yù)期的用例時序圖作對比，就可以判斷出狀態(tài)圖是否滿足業(yè)務(wù)需求。

對象在執(zhí)行過程中所產(chǎn)生的Event 序列，如果與預(yù)期定義的用例時序圖中的事件交互順序不一致，則表明對象業(yè)務(wù)需求未得到滿足。

3 實驗驗證

文中驗證了一個列車管理域模型，該域的類模型如圖3 所示。

圖3 列車管理的類圖

由類圖可知，一個列車運行的一個路段(Hop)包括多個加速曲線(AccelerationCurve)。

對AccelerationCurve 的對象建立如圖4 所示的狀態(tài)圖。

圖4 AccelerationCurve 對象的狀態(tài)圖

分別為MaintainingAccelerationCurve 狀態(tài)和A ccelerationCurveComplete 狀態(tài)添加用入口動作，下面給出用ASL 描述的MaintainingAccelerationCurve 狀態(tài)的入口動作，整個入口動作用于判斷AccelerationCurve對象是否到達了加速曲線終點。

AccelerationCurveComplete 狀態(tài)中的入口動作描述了列車如何從一個加速曲線過度到另個一個加速曲線。

運行信號事件驅(qū)動框架，在狀態(tài)解析部分驗證了狀態(tài)圖的體系結(jié)構(gòu)，SCXML 表示的體系結(jié)構(gòu)滿足條件1 ～條件3，AccelerationCurve 對象的性能需求合理。

用ASL 來表示外部激勵信號，該信號模擬了Hop對象對AccelerationCurve 對象的激勵。

在輸入事件觸發(fā)按鈕響應(yīng)的對話框中輸入用ASL描述的測試例程:generate performCurve()to theAccelerationCurve。如圖5 所示。

圖5 狀態(tài)圖業(yè)務(wù)需求驗證

點擊確定后得到對象在生命期內(nèi)的行為過程，執(zhí)行結(jié)果如圖6 所示。

圖6 AccelerationCurve 對象的執(zhí)行結(jié)果

從執(zhí)行信息里可了解到該對象在其生命期內(nèi)的信號事件序列，它表示對象在經(jīng)過速度調(diào)節(jié)之后到達了路段的終點，并向Hop 對象發(fā)送了完成信號。將其與預(yù)期的用例時序圖做比較，就可以判斷出狀態(tài)圖是否表現(xiàn)出了應(yīng)有的業(yè)務(wù)需求。

4 結(jié)束語

本文給出了一種驗證SysML 狀態(tài)圖合理性的實現(xiàn)方案。用SCXML 和ASL 精確無歧義描述SysML 狀態(tài)圖，通過信號事件驅(qū)動機制完成體系結(jié)構(gòu)和業(yè)務(wù)需求的驗證。

將SysML 狀態(tài)圖作為行為模型并不完全［7－9］，而且在體系結(jié)構(gòu)驗證部分沒有考慮并發(fā)工作流和時序邏輯［10］方面的內(nèi)容。本文以后的一個研究方向是:對SysML 狀態(tài)圖進行時間拓展，給出拓展后的SysML 狀態(tài)圖到時間自動機的過程，使用時間計算樹邏輯［11］表示時序約束，并驗證時序約束的一致性。

［1］ 蔣彩云，王維平，李群.SysML:一種新的系統(tǒng)建模語言［J］.系統(tǒng)仿真學報，2006，18(6):1483－1487，1492.

［2］ JIM B G.State chart XML(SCXML):state machine notation for control abstraction［S］.USA:Voice Browser，2013.

［3］ CHRIS R，PAUL F.Model driven architecture with executable UML［M］.北京:機械工業(yè)出版社，2006.

［4］ 陸公正.基于UML 狀態(tài)圖的工作流建模與驗證［D］.蘇州:蘇州大學，2006.

［5］ VERBEEK H M W.Diagnosing workflow process using woflan［J］.Computer Journal，2001，44(4):246－279.

［6］ KWON G.Rewrite rules and operational semantics for model checking UML statecharts［C］.Berlin:Lecture Notes In Computer Science，Springer，2000.

［7］ GNESI S，MAZZANTI F.A model checking verification environment for UML statecharts［C］.Udine:XLIII Annual Italian Conference AICA，IEEE Computer Society，2005.

［8］ ESHUIS R.Symbolic model checking of UML activity diagrams［J］.ACM Transactions on Software Engineering and Methodology，2006(15):1－38.

［9］ 李廣元，唐稚松.基于線性時序邏輯的實時系統(tǒng)模型檢查［J］.軟件學報，2002，13(2):193－202.

［10］ALUR R，HENZINGER T A.Logics and models of real time:a survey［M］.Berlin:Springer－Verlag，1992.

［11］杜杰，江國華.基于模型檢測的UML 狀態(tài)圖和順序圖一致性檢測［J］.電子科技，2012，25(2):100－104.