李 勇，曹子寧

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

基于需求的形式化建模與驗(yàn)證方法研究

李 勇，曹子寧

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

軟件開(kāi)發(fā)過(guò)程中需求階段的錯(cuò)誤比設(shè)計(jì)或?qū)崿F(xiàn)階段所引入的錯(cuò)誤對(duì)系統(tǒng)的安全性與可靠性有更大的影響。為了能夠在早期發(fā)現(xiàn)錯(cuò)誤，降低開(kāi)發(fā)成本，精確、簡(jiǎn)明地驗(yàn)證和規(guī)范軟件系統(tǒng)和性質(zhì)，在模型的形式化開(kāi)發(fā)方法和模型檢測(cè)的自動(dòng)驗(yàn)證技術(shù)的研究基礎(chǔ)上，提出了一種基于需求的形式化建模與驗(yàn)證的框架。運(yùn)用基于四變量模型的需求狀態(tài)機(jī)語(yǔ)言RSML-e建立了形式化模型，并給出了形式化的轉(zhuǎn)換規(guī)則，將RSML-e模型轉(zhuǎn)換為模型檢測(cè)器NuSMV的輸入模型，并進(jìn)行了檢測(cè)，建立起了一套整體的形式化開(kāi)發(fā)框架，并以航空電子系統(tǒng)特定實(shí)例進(jìn)行了建模與驗(yàn)證。驗(yàn)證結(jié)果表明，已建航電系統(tǒng)模型的安全性和可靠性是有效的。

形式化方法;RSML-e;模型檢測(cè);NuSMV

0 引 言

隨著軟件系統(tǒng)日益增長(zhǎng)的復(fù)雜性和系統(tǒng)集成的問(wèn)題，潛在的錯(cuò)誤不斷增加并可能影響到系統(tǒng)的安全性和可靠性。傳統(tǒng)的軟件工程方法已經(jīng)很難滿足需求，迫切需要新的方法來(lái)設(shè)計(jì)開(kāi)發(fā)安全性更高、開(kāi)發(fā)成本更低的大型復(fù)雜系統(tǒng)。為了解決這些實(shí)際問(wèn)題，形式化開(kāi)發(fā)方法在系統(tǒng)開(kāi)發(fā)過(guò)程中被廣泛應(yīng)用，通過(guò)給出需求描述嚴(yán)格的形式定義，設(shè)計(jì)可執(zhí)行的原型系統(tǒng)，然后通過(guò)模型檢測(cè)以及新興的代碼自動(dòng)生成等形式化技術(shù)的運(yùn)用，大大提升了系統(tǒng)的安全性和可靠性，同時(shí)也大大節(jié)省了時(shí)間和成本[1-2]。目前面向需求形式化方法的研究也是形式化方法研究的熱點(diǎn)。文獻(xiàn)[3]借鑒π演算的進(jìn)程構(gòu)造能力和類(lèi)型系統(tǒng)表達(dá)能力，以π演算為需求建模語(yǔ)言，提出一種需求建模的形式化方法，給出構(gòu)造功能行為交互系統(tǒng)的良類(lèi)型性質(zhì)。文獻(xiàn)[4]提出了一種面向航天嵌入式系統(tǒng)的名為SPARDL的形式化建模方法，還設(shè)計(jì)了代碼生成方法。文獻(xiàn)[5]提出了一種基于UML-NuSMV需求建模方法，并用該方法對(duì)列控系統(tǒng)的安全性進(jìn)行了分析。

在形式化方法研究的基礎(chǔ)上，運(yùn)用需求狀態(tài)機(jī)語(yǔ)言RSML-e對(duì)系統(tǒng)進(jìn)行形式化需求規(guī)約，創(chuàng)建系統(tǒng)的形式化模型，在建模過(guò)程中能夠發(fā)現(xiàn)大量系統(tǒng)描述中的錯(cuò)誤，而且能夠作為與用戶交互的實(shí)模型，并能夠以仿真的形式向客戶執(zhí)行。但RSML-e不支持直接的模型檢測(cè)[6]。

為此，將模型轉(zhuǎn)換為以工具直接驗(yàn)證的形式化模型，選取已經(jīng)十分成熟的NuSMV符號(hào)化模型檢測(cè)工具，給出模型的形式化轉(zhuǎn)換規(guī)則，將RSML-e的規(guī)格說(shuō)明通過(guò)形式化轉(zhuǎn)換規(guī)則換為NuSMV的輸入模型，并規(guī)約航空電子系統(tǒng)的飛行導(dǎo)航系統(tǒng)的屬性，用建立的基于需求的形式化建模與驗(yàn)證框架對(duì)其進(jìn)行了實(shí)驗(yàn)驗(yàn)證。結(jié)果表明，已建系統(tǒng)模型的安全性和可靠性是有效的，為進(jìn)一步開(kāi)發(fā)可靠安全的系統(tǒng)奠定了基礎(chǔ)。

1 背景簡(jiǎn)介

1.1 RSML-e

RSML(Request State Machine Language，需求狀態(tài)機(jī)語(yǔ)言)是由加州大學(xué)的Nancy Leveson研究組開(kāi)發(fā)的一種基于狀態(tài)的描述語(yǔ)言，用于對(duì)過(guò)程控制系統(tǒng)的行為建模。在研究過(guò)程中，為了解決顯式事件的依賴性引入的錯(cuò)誤，美國(guó)的明尼蘇達(dá)大學(xué)關(guān)鍵系統(tǒng)組開(kāi)發(fā)了RSML-e(RSML沒(méi)有顯式事件)，消除了顯式事件且是同步語(yǔ)言[7]。

和SCR方法類(lèi)似，RSML-e也是基于四變量方法[8]的思想，是基于狀態(tài)機(jī)的形式化建模語(yǔ)言。RSML-e語(yǔ)言易讀易理解，能夠讓客戶更多地參與到系統(tǒng)開(kāi)發(fā)中，從而實(shí)現(xiàn)設(shè)計(jì)人員和客戶之間對(duì)于需求描述的理解的一致性。RSML-e形式化地描述了系統(tǒng)的行為模型，能夠方便地轉(zhuǎn)換為定理自動(dòng)證明和模型檢測(cè)的輸入形式，使模型可執(zhí)行，通過(guò)模型檢測(cè)和定理自動(dòng)證明來(lái)保證系統(tǒng)行為的完備性和一致性，從而提升系統(tǒng)的安全性?；谶@種需求描述的需求形式化分析方法，可以在需求階段找出大量錯(cuò)誤，大大減少后續(xù)排錯(cuò)的工作和時(shí)間消耗。

1.2 NuSMV

模型檢測(cè)的基本思想將系統(tǒng)行為抽象為一個(gè)有限狀態(tài)機(jī)M，系統(tǒng)約束規(guī)范使用時(shí)序邏輯公式F表示。狀態(tài)遷移系統(tǒng)M是否具有所期望的性質(zhì)，可以用公式Μ|=?F表示[9]。模型檢測(cè)面臨的一個(gè)重大問(wèn)題是狀態(tài)爆炸，為了解決該問(wèn)題，引入二元決策圖，以符號(hào)表示狀態(tài)空間。雖然還是有狀態(tài)空間的大小限制，但符號(hào)模型檢測(cè)器可以比顯式狀態(tài)模型檢測(cè)更大的狀態(tài)空間。

CMU和IRST聯(lián)合開(kāi)發(fā)的符號(hào)模型檢測(cè)工具NuSMV，用于檢測(cè)有限狀態(tài)系統(tǒng)是否滿足CTL約束公式。NuSMV是一種開(kāi)放的模型檢測(cè)結(jié)構(gòu)，它可以可靠地用于工業(yè)設(shè)計(jì)的驗(yàn)證，執(zhí)行過(guò)程為用戶將表示系統(tǒng)模型和約束規(guī)范的SMV程序作為輸入，NuSMV自動(dòng)檢測(cè)約束規(guī)則在模型檢測(cè)中是否成立，若成立則輸出true，否則輸出false，并給出反例。

NuSMV2擴(kuò)展了以前版本的NuSMV幾個(gè)新特性，尤其是與執(zhí)行的可能性SAT-based有界模型檢查,釋放提供了一些新功能，許多錯(cuò)誤修復(fù)和優(yōu)化，大量不同的軟件建筑和建筑系統(tǒng)，是NuSMV新模型檢測(cè)算法和延伸技術(shù)，允許一個(gè)更強(qiáng)大的操作模型，可以生成平面模型對(duì)整個(gè)語(yǔ)言，同時(shí)也允許錐的影響減少。所給出的模型轉(zhuǎn)換規(guī)則主要適用于最新版本的NuSMV工具[10]。

2 形式化建模與驗(yàn)證框架

首先給出需求模型、模型轉(zhuǎn)換、模型檢測(cè)的一般框架，如圖1所示。

圖1 形式化建模與驗(yàn)證框架

2.1 RSML-e模型

一個(gè)RSML-e描述由變量、狀態(tài)、轉(zhuǎn)移、功能函數(shù)、宏、常量和接口組成[11]。需求描述中的變量用于存儲(chǔ)外部傳感器的輸入值，也用于暫存系統(tǒng)的輸出值。RSML-e以分層的形式組織狀態(tài)，其中狀態(tài)轉(zhuǎn)移由一個(gè)原狀態(tài)，一個(gè)目的狀態(tài)，一個(gè)觸發(fā)事件，一個(gè)監(jiān)督條件和一組動(dòng)作事件組成，控制著一個(gè)狀態(tài)到其他狀態(tài)的轉(zhuǎn)移。為了執(zhí)行一次狀態(tài)轉(zhuǎn)移，當(dāng)觸發(fā)事件發(fā)生時(shí)監(jiān)督條件同時(shí)為真。監(jiān)督條件是在不同的狀態(tài)和變量之間的一種謂詞邏輯表達(dá)式。為了克服命題邏輯符號(hào)語(yǔ)言的復(fù)雜性問(wèn)題，RSML-e使用析取范式(DNF)來(lái)表示，這種表格稱為AND/OR表[12]。AND/OR表格的最左一列列出了邏輯短語(yǔ)。其他的列是這些邏輯短語(yǔ)的連接，并且列出了表達(dá)式的邏輯真值。規(guī)定只要有某一列的值為真，則整個(gè)表的值就為真。而每列的真值為真當(dāng)且僅當(dāng)此列的真值與它們所關(guān)聯(lián)的邏輯短語(yǔ)的真值都一致。圖2為ANDOR表等同于DNF范式(Condition1∧Condition2)，‘*’表示不關(guān)心條件的真假。

圖2 RSML-e中的ANDOR

2.2 NuSMV的輸入與輸出

SMV程序由一個(gè)或多個(gè)模塊構(gòu)成，和C語(yǔ)言一樣，其中一個(gè)模塊必須稱為main，模塊可以聲明變量并賦值，程序最后給出要驗(yàn)證的性質(zhì)，用CTL公式描述。如下給出了一段NuSMV程序的示例，包括主模塊和要驗(yàn)證的性質(zhì)。

MODULE main

VAR

request：boolean;

status:{ready,busy}

ASSIGN

init(status):=ready ;

next(status):=

case

reuqest:busy;

1:{ready,busy};

esac;

CTLSPEC

AG(request->status=busy);

2.3 轉(zhuǎn)換規(guī)則

2.3.1 類(lèi)型和變量的轉(zhuǎn)換

RSML-e不僅支持布爾型、枚舉型、整型、實(shí)型等基本的數(shù)據(jù)類(lèi)型，還支持用戶自定義的類(lèi)型，但NuSMV不支持用戶自定義的類(lèi)型，所以RSML-e中自定義的類(lèi)型就要轉(zhuǎn)換為枚舉等基本數(shù)據(jù)類(lèi)型[13]。RSML-e中的輸入和狀態(tài)變量轉(zhuǎn)換為NuSMV時(shí)，用關(guān)鍵詞VAR表示為：

VAR identifier_name:var_type;

2.3.2 宏的轉(zhuǎn)換

RSML-e中的宏對(duì)應(yīng)轉(zhuǎn)換為NuSMV中的一個(gè)子模塊，可以做一一對(duì)應(yīng)的轉(zhuǎn)換，RSML-e對(duì)應(yīng)的參數(shù)應(yīng)保持轉(zhuǎn)換，在NuSMV的子模塊添加參數(shù)，此外，子模塊必須在主模塊中添加聲明。

2.3.3 相對(duì)時(shí)間概念

RSML-e中用PREV的前綴表示當(dāng)前研究狀態(tài)的前狀態(tài)，但NuSMV中只有next關(guān)鍵字表示后狀態(tài)，所以在做對(duì)應(yīng)轉(zhuǎn)換時(shí)應(yīng)將帶有PREV前綴的狀態(tài)描述為NuSMV中的當(dāng)前狀態(tài)，而不帶前綴的描述為NuSMV中的后狀態(tài)，在后面的實(shí)例中加以說(shuō)明。

3 ASW具體實(shí)例

結(jié)合飛機(jī)系統(tǒng)中的高度按鈕(Altitude Switch，ASW)的實(shí)例來(lái)說(shuō)明轉(zhuǎn)換規(guī)則。ASW的主要功能為接收的輸入有禁止設(shè)備啟動(dòng)信號(hào)，系統(tǒng)重置信號(hào)，以及飛機(jī)的實(shí)時(shí)飛行高度，并當(dāng)飛機(jī)的飛行高度低于某個(gè)閾值時(shí)，ASW按鈕控制相關(guān)設(shè)備(Device Of Interest,DOI)的啟動(dòng)與觸發(fā)，如圖3所示的實(shí)例框架。

圖3 ASW抽象框架

針對(duì)ASW，運(yùn)用RSML-e進(jìn)行建模。其中變量聲明部分應(yīng)包括輸入變量高度的數(shù)據(jù)變量、禁止信號(hào)的變量、重置信號(hào)的變量，以及ASW的狀態(tài)變量，圖4給出高度變量和ASW狀態(tài)變量的RSML-e模型。

VARaltitude

Type:real

InitialValue:UNDEFINED

Classifiedas:MONITORED

狀態(tài)變量ASW：

STATE_VARIABLEASW

Type:{OFF,ON}

InitialValue:OFF

Classifiedas:State

圖4 高度變量和ASW狀態(tài)變量的RSML-e模型

模型中宏的聲明包括對(duì)禁止和重置兩個(gè)信號(hào)定義兩個(gè)宏，判斷高度值是否低于指定閾值的宏，這里給出禁止信號(hào)的宏以及系統(tǒng)的輸出ASW宏：

MACRO when_inhibit_Pressed

Condition:

When(inhibit=ON);

MACRO when_ASW_Power_ON

Condition:

When(ASW=ON);

模型建立完成，接下來(lái)將模型轉(zhuǎn)換為NuSMV的輸入模型，根據(jù)第2節(jié)的變量轉(zhuǎn)換規(guī)則，對(duì)VAR關(guān)鍵字定義的變量可以轉(zhuǎn)換為：

MODULE main

VAR

altitude：real;

VAR

ASW:{OFF,ON};

ASSIGN

init(ASW):=OFF;

next(ASW):=

case

!m_when_inhibit_Pressed.result() & !m_when_inhibit_Pressed.result() &

m_when_altitide_below():ON;

m_when_inhibit_Pressed.result()|m_when_inhibit_Pressed.result() |

m_when_altitide_below():OFF;

esac;

根據(jù)宏的形式化轉(zhuǎn)換規(guī)則，宏when_inhibit_Pressed轉(zhuǎn)換為：

MODULEwhen_inhibit_Pressed()

VAR

result:boolean;

ASSIGN

init(result):=FLASE;

next(result):=When(inhibit=ON);

MODULE main

m_when_inhibit_Pressed: when_inhibit_Pressed()//主模式中的聲明部分

驗(yàn)證其安全性和可靠性屬性，給出其要驗(yàn)證的CTL邏輯公式[14]，給出安全性和活性兩個(gè)驗(yàn)證的示例：

CTLSPEC

AG((Inhibit=TRUE)->m_when_ASW_Power_ON.result=TRUE)

AG((Reset=TRUE)->m_when_ASW_Power_ON.result=FLASE)

用NuSMV工具驗(yàn)證得到的結(jié)果如下：

--specification AG((Inhibit=TRUE->m_when_ASW_Power_ON.result=TRUE) is true

--specification AG((Reset=TRUE)->m_when_ASW_Power_ON.result=FLASE) is true

模型檢測(cè)器NuSMV對(duì)示例中兩個(gè)邏輯公式驗(yàn)證結(jié)果返回為true，表明建立的RSML模型滿足示例中的兩個(gè)屬性，否則會(huì)給出反例。后續(xù)可對(duì)更多的安全性和活性的屬性進(jìn)行驗(yàn)證。

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

將基于需求的形式化方法應(yīng)用在航電領(lǐng)域，基于需求建模語(yǔ)言RSML-e對(duì)飛行導(dǎo)航系統(tǒng)進(jìn)行建模，并用模型檢測(cè)器NuSMV對(duì)其進(jìn)行形式化的模型轉(zhuǎn)換與驗(yàn)證。具體實(shí)例的運(yùn)行結(jié)果表明，所建立的模型滿足安全性和可靠性，能夠滿足航電的技術(shù)要求。后續(xù)研究可將需求建模、體系結(jié)構(gòu)建模相結(jié)合，將形式化方法運(yùn)用于系統(tǒng)開(kāi)發(fā)的各個(gè)階段，從而給出從需求到驗(yàn)證的一套完整的系統(tǒng)的形式化開(kāi)發(fā)框架。

[1] 呂 毅.形式化方法介紹及其在工程中的應(yīng)用[J].微電子學(xué)與計(jì)算機(jī),2003,20(10):26-31.

[2] 張廣泉.關(guān)于軟件形式化方法[J].重慶師范學(xué)院學(xué)報(bào):自然科學(xué)版,2002,19(2):1-4.

[3] 雷義偉,賁可榮,何智勇.自適應(yīng)軟件需求的形式化建模與驗(yàn)證[J].海軍工程大學(xué)學(xué)報(bào),2015,27(6):73-78.

[4] 顧 斌,董云衛(wèi),王 政.面向航天嵌入式軟件的形式化建模方法[J].軟件學(xué)報(bào),2015,26(2):321-331.

[5] 周玉平.基于UML-NuSMV模型的列控系統(tǒng)需求階段的安全分析[D].北京:北京交通大學(xué),2015.

[6] Jordan H,Beecham S,Botterweck G.Modelling software engineering research with RSML[C]//Proceedings of the 18th international conference on evaluation and assessment in software engineering.[s.l.]:ACM,2014:1-10.

[7] Choi Y,Heimdahl M P E.Model checking RSML-e,requirements[C]//International symposium on high assurance systems engineering.[s.l.]:IEEE,2002:109-118.

[8] Miller S P,Tribble A C.Extending the four-variable model to bridge the system-software gap[C]//Digital avionics systems.[s.l.]:[s.n.],2001.

[9] 楊 軍,葛海通,鄭飛君,等.一種形式化驗(yàn)證方法:模型檢驗(yàn)[J].浙江大學(xué)學(xué)報(bào):理學(xué)版,2006,33(4):403-407.

[10] 呂 審.NuSMV模型檢測(cè)的研究及應(yīng)用[D].武漢:武漢理工大學(xué),2011.

[11] Cavada R,Cimatti A.NuSMV 2.6 manual[M].[s.l.]:[s.n.],2010.

[12] Miller S,Tribble A,Whalen M,et al.Proving the shalls[J].International Journal on Software Tools for Technology Transfer,2006,8(4-5):303-319.

[13] Heimdahl M P E，Leveson N G，Reese J D.Experience from specifying the TCASⅡ requirements using RSML[C]//Digital avionics systems conference.[s.l.]:[s.n.],2005.

[14] 鮑秋霜,張晉津.直覺(jué)主義計(jì)算樹(shù)邏輯中的安全性和活性[J].計(jì)算機(jī)科學(xué)與探索,2016,10(2):163-172.

Investigation on Formal Modeling and Verification Method Based on Specification

LI Yong,CAO Zi-ning

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

In the process of software development,the mistakes introduced in requirements phase have a more significant effect of the security and reliability than the phase of designing.In order to be able to detect the errors in the early phase of the software development and reduce development costs,and to describe the software system precisely and concisely,a formal modeling and verification framework has been proposed with the technology of automatic verification,in which the RSML-emodel has been used and then the formal transformation rules have been given.Based on these rules,the proposed model can be transformed into the input model of the NuSMV,which is performed in model checking of the system.The specific instances of avionics system have been employed to implement modeling test experiments for verification.The experimental results show that the security and reliability of the established avionics system have been verified to be effective.

formal method;RSML-e;model checking;NuSMV

2016-06-30

2016-10-13 網(wǎng)絡(luò)出版時(shí)間：2017-04-28

國(guó)家“973”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃項(xiàng)目(2014CB744900);航空科學(xué)基金(20150652008)

李 勇(1990-)，男，碩士生，研究方向?yàn)樾问交椒?曹子寧，教授，博士生導(dǎo)師，研究方向?yàn)樾问交椒?、人工智能?/p>

http://kns.cnki.net/kcms/detail/61.1450.TP.20170428.1702.034.html

TP31

A

1673-629X(2017)06-0007-04

10.3969/j.issn.1673-629X.2017.06.002