基于NuSMV的SysML模型形式化驗(yàn)證

鄧劉夢(mèng)，葛曉瑜，宛偉健

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106)

0 引 言

在過去多年，軟件開發(fā)面臨了多個(gè)挑戰(zhàn)，新的需求和存在系統(tǒng)不斷增長(zhǎng)，系統(tǒng)也變得越來越復(fù)雜，以至于很難及時(shí)地對(duì)它們進(jìn)行構(gòu)建。為了解決這些問題，出現(xiàn)了很多新的方法，其中最突出的一個(gè)就是模型驅(qū)動(dòng)開發(fā)。

模型驅(qū)動(dòng)開發(fā)代表了一套理論和工業(yè)化軟件開發(fā)的方法框架，在軟件開發(fā)全生命周期中系統(tǒng)的使用模型作為主要工件，主要是為了解決軟件的兩個(gè)根本危機(jī)：復(fù)雜性和變更能力。但與此同時(shí)，模型驅(qū)動(dòng)開發(fā)也帶來了一些問題：使用自然語言描述的需求與嚴(yán)格定義的模型之間的鴻溝無法很好地連通[1]。此外，對(duì)于SysML描述的圖形化模型，目前缺乏嚴(yán)格有效的分析和驗(yàn)證方法。

針對(duì)以上存在的問題，文中給出了從SysML模型到NuSMV輸入模型的轉(zhuǎn)換規(guī)則，并實(shí)現(xiàn)自動(dòng)化程序完成這一轉(zhuǎn)換。接著利用NuSMV模型檢測(cè)的方法來驗(yàn)證SysML模型的正確性。

1 SysML系統(tǒng)建模

SysML是目前業(yè)界常用的系統(tǒng)體系結(jié)構(gòu)建模語言，可用于由軟硬件、數(shù)據(jù)和人綜合而成的復(fù)雜系統(tǒng)的分析與設(shè)計(jì)。然而，為了保證一定的易讀性，SysML采用半形式化的描述方法來定義語義，使用自然語言描述約束和詳細(xì)語義，力求在形式嚴(yán)格和易于理解間找到平衡[2]。在實(shí)際中，其圖形化的建模方式十分簡(jiǎn)潔直觀，關(guān)系鏈接與約束描述等方式也進(jìn)一步縮小了模型驅(qū)動(dòng)開發(fā)過程中需求描述與模型設(shè)計(jì)制品間的溝壑。但是，其犧牲的部分就是缺乏精確的語義，難以進(jìn)行嚴(yán)格的語義分析以及正確性驗(yàn)證。

SysML是一種圖形化建模語言，是對(duì)象管理組織(object management group，OMG)在對(duì)UML2.0的子集進(jìn)行重用和擴(kuò)展的基礎(chǔ)上提出的一種新建模語言[3]。它為軟件體系結(jié)構(gòu)建模提供了豐富的圖標(biāo)，涵蓋了從系統(tǒng)需求到設(shè)計(jì)階段的各項(xiàng)要求，廣泛應(yīng)用于航空航天軟件開發(fā)過程。它致力于建模具有眾多組件、難以描述、理解、預(yù)測(cè)、管理、設(shè)計(jì)以及更改的系統(tǒng)，并提供了表達(dá)個(gè)人需求及其組成的手段，已被學(xué)術(shù)界和工業(yè)界所廣為接受，作為一種標(biāo)準(zhǔn)建模語言[4]。

SysML為系統(tǒng)的結(jié)構(gòu)模型、行為模型、需求模型和參數(shù)模型定義了語義。結(jié)構(gòu)模型強(qiáng)調(diào)系統(tǒng)的層次以及對(duì)象之間的相互連接關(guān)系，包括類和裝配。行為模型強(qiáng)調(diào)系統(tǒng)中對(duì)象的行為，包括它們的活動(dòng)、交互和狀態(tài)歷史[5]。

文中主要使用SysML的塊定義圖對(duì)系統(tǒng)的靜態(tài)結(jié)構(gòu)進(jìn)行描述，使用狀態(tài)機(jī)圖對(duì)系統(tǒng)的動(dòng)態(tài)遷移進(jìn)行描述。SysML中，塊(block)是系統(tǒng)描述的最小建模單位，可以用來描述每一個(gè)單獨(dú)的組件，同時(shí)也是描述系統(tǒng)結(jié)構(gòu)特征和行為特征的單元。SysML塊以UML類圖為基礎(chǔ)，并擴(kuò)展了UML復(fù)合結(jié)構(gòu)的一些特征[6]。塊定義圖(block definition diagram)則是用于描述塊信息的圖。它描述了塊的屬性值、塊的組成部分、塊的操作以及對(duì)其他塊的參考等[7]。而狀態(tài)機(jī)圖(state machine diagram)則是用來描述系統(tǒng)的狀態(tài)遷移情況[8]。其中狀態(tài)轉(zhuǎn)移用來描述對(duì)象對(duì)事件的響應(yīng)情況。關(guān)于SysML塊定義圖以及狀態(tài)機(jī)圖的實(shí)例將在下一節(jié)給出。

2 NuSMV模型

針對(duì)SysML模型進(jìn)行驗(yàn)證，采用NuSMV作為驗(yàn)證工具。

2.1 輸入語言分析

NuSMV模型中，系統(tǒng)被描述為模塊化的層次結(jié)構(gòu)，支持定義組件的重用[9]。其支持的數(shù)據(jù)類型主要有枚舉類型、布爾類型和固定數(shù)組等?；旧?，一個(gè)完整的NuSMV模型文件主要由兩部分組成：系統(tǒng)模型和待驗(yàn)證的系統(tǒng)性質(zhì)[10-11]。

NuSMV系統(tǒng)模型部分主要用于描述系統(tǒng)的狀態(tài)以及狀態(tài)遷移關(guān)系，刻畫出系統(tǒng)的靜態(tài)結(jié)構(gòu)與動(dòng)態(tài)行為[12]。通過關(guān)鍵字MODULE來定義模塊，通常每一個(gè)模塊對(duì)應(yīng)一個(gè)系統(tǒng)組件[13]。通過主模塊中的SPEC字段進(jìn)行待驗(yàn)證需求性質(zhì)描述，同時(shí)支持計(jì)算樹邏輯(computation tree logic，CTL)和線性時(shí)序邏輯(linear-time temporal，LTL)的表達(dá)式[14-15]。

2.2 SysML模型到NuSMV模型的轉(zhuǎn)換

本節(jié)根據(jù)SysML模型與NuSMV模型的特點(diǎn)[16]，給出轉(zhuǎn)化規(guī)則，并實(shí)現(xiàn)工具完成NuSMV模型實(shí)例的自動(dòng)化生成。

首先對(duì)SysML中的靜態(tài)圖進(jìn)行轉(zhuǎn)換，文中主要使用的是塊定義圖。

規(guī)則1：模塊名聲明。

描述：對(duì)于NuSMV中的模塊名根據(jù)塊定義圖中的名稱進(jìn)行命名。

規(guī)則2：靜態(tài)變量聲明。

描述：對(duì)于塊定義圖中定義的屬性都須在相應(yīng)的模塊中通過VAR關(guān)鍵字進(jìn)行聲明。

規(guī)則3：變量初值。

描述：對(duì)于塊定義圖中所有屬性的初值都須在相應(yīng)的模塊中通過ASSIGN關(guān)鍵字進(jìn)行聲明。

接下來對(duì)SysML中的動(dòng)態(tài)行為模型進(jìn)行轉(zhuǎn)換。SysML中主要通過狀態(tài)機(jī)圖對(duì)系統(tǒng)的狀態(tài)遷移進(jìn)行刻畫，系統(tǒng)中可能出現(xiàn)的狀態(tài)遷移，都存在對(duì)應(yīng)的狀態(tài)機(jī)圖[12]。從另一個(gè)側(cè)面來看，狀態(tài)圖也可以理解為對(duì)塊定義圖動(dòng)態(tài)的補(bǔ)充，故在轉(zhuǎn)換中，應(yīng)將其放入相應(yīng)的模塊中，而不是重新聲明模塊。

規(guī)則4：狀態(tài)機(jī)圖聲明。

描述：對(duì)于狀態(tài)機(jī)圖轉(zhuǎn)換不重新進(jìn)行模塊聲明，將其狀態(tài)遷移關(guān)系通過TRANS、next等關(guān)鍵字描述加入到從屬的塊定義圖對(duì)應(yīng)的模塊中。

例如：Car對(duì)應(yīng)的狀態(tài)機(jī)圖，其描述的狀態(tài)遷移關(guān)系都應(yīng)該加入到MODULE car中。

規(guī)則5：狀態(tài)變量聲明。

描述：如果一個(gè)塊定義圖存在一個(gè)對(duì)應(yīng)的狀態(tài)機(jī)圖，則應(yīng)該在此塊對(duì)應(yīng)的模塊中通過VAR聲明一個(gè)state變量。

規(guī)則6：狀態(tài)變量賦值。

描述：狀態(tài)機(jī)圖中state的取值是由去除初始狀態(tài)和結(jié)束狀態(tài)后所有狀態(tài)值構(gòu)成的枚舉集合，其初始值應(yīng)為狀態(tài)機(jī)圖中Initial節(jié)點(diǎn)指向的第一個(gè)狀態(tài)，通過ASSGIN聲明。

例如：對(duì)于汽車car，通過一個(gè)狀態(tài)機(jī)圖描述其運(yùn)行狀態(tài)可能存在運(yùn)行或者停止兩種狀態(tài)(見圖1)，那么MODULE car中VAR字段就需加入car_state:{stop，running}聲明，初始狀態(tài)為stop，通過ASSGIN init(car_state):=stop字段進(jìn)行聲明。

圖1 汽車運(yùn)行狀態(tài)機(jī)圖實(shí)例

規(guī)則7：狀態(tài)遷移。

描述：狀態(tài)機(jī)圖確定的狀態(tài)轉(zhuǎn)變使用next進(jìn)行描述，并通過case來表達(dá)分支情況。

例如：car_state當(dāng)前狀態(tài)為stop下一狀態(tài)為running和當(dāng)前狀態(tài)為running下一狀態(tài)為stop表示如下：

next(car_state):=

case

car_state=stop:{running};

car_state=running:{stop};

esac

規(guī)則8：狀態(tài)遷移條件。

描述：如果狀態(tài)機(jī)圖中的狀態(tài)遷移存在遷移條件，則需將該守衛(wèi)條件加入到遷移描述字段中(見圖2)。

例如：在汽車啟動(dòng)前應(yīng)確定車門是關(guān)閉的，否則無法啟動(dòng)。

next(car_state):=

car_state=stop&door.closed=1:{running};

圖2 存在守衛(wèi)條件的狀態(tài)遷移實(shí)例

3 實(shí)驗(yàn)與案例分析

根據(jù)前幾節(jié)的理論分析，實(shí)現(xiàn)了一個(gè)SysML模型到NuSMV模型自動(dòng)轉(zhuǎn)換的工具。下面通過案例演示。

案例的場(chǎng)景如下：在鐵路控制系統(tǒng)中，在火車通過路口時(shí)需要關(guān)閉公路兩側(cè)的柵欄，保證在火車通過的過程中汽車無法駛?cè)肼房?，避免發(fā)生火車汽車相撞的事故。首先通過SysML建模工具建立該場(chǎng)景的模型如下：

圖3 鐵路案例SysML塊定義圖

圖3中塊定義圖描述了系統(tǒng)的靜態(tài)結(jié)構(gòu)信息，圖4中狀態(tài)機(jī)圖則描述了系統(tǒng)的狀態(tài)以及遷移關(guān)系。

圖4 鐵路案例SysML狀態(tài)機(jī)圖

在建模分別得到塊定義圖和狀態(tài)機(jī)圖后，利用工具將模型導(dǎo)出為XMI文件格式以供后續(xù)轉(zhuǎn)換使用。接著將得到的SysML模型文件輸入到自動(dòng)轉(zhuǎn)換工具中即可完成轉(zhuǎn)換，得到鐵路系統(tǒng)的SMV文件(見圖5)。

圖5 SysML模型轉(zhuǎn)換工具界面

得到設(shè)計(jì)模型的實(shí)例后，即可利用已有的NuSMV工具來檢測(cè)系統(tǒng)需求是否被設(shè)計(jì)模型所實(shí)現(xiàn)。首先給出一條安全需求：該系統(tǒng)模型不得出現(xiàn)汽車和火車同時(shí)駛?cè)肼房诘那闆r，避免事故發(fā)生。接著在得到的SMV文件中寫入該需求性質(zhì)LTL表達(dá)式：LTLSPEC G!((Car_state=Car_in) & (Train_state= Train_in))。最后在Windows10下采用命令行形式運(yùn)行NuSMV工具檢測(cè)該SMV文件得到的結(jié)果如圖6所示。

圖6 需求驗(yàn)證結(jié)果

得到LTL公式檢測(cè)結(jié)果為false,即該需求沒有被滿足。NuSMV工具給出了反例，觀察到在1.5狀態(tài)時(shí)同時(shí)出現(xiàn)了汽車和火車均進(jìn)入路口的情況。

同時(shí)表明文中轉(zhuǎn)換工具得到的SMV文件可以很好地作為NuSMV工具的輸入，證明了該方法的有效性。

4 結(jié)束語

針對(duì)SysML模型缺乏精確語義而難以進(jìn)行模型正確性驗(yàn)證的問題，給出了一個(gè)通過模型轉(zhuǎn)換技術(shù)實(shí)現(xiàn)模型驗(yàn)證的解決方法。實(shí)現(xiàn)了一個(gè)從SysML設(shè)計(jì)模型到NuSMV模型自動(dòng)轉(zhuǎn)換的工具，最后利用轉(zhuǎn)換得到的SMV文件作為模型檢測(cè)器的輸入即可進(jìn)行SysML模型的驗(yàn)證。