李 勇，曹子寧

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

基于需求的形式化建模與驗證方法研究

李 勇，曹子寧

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

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

形式化方法;RSML-e;模型檢測;NuSMV

0 引 言

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

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

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

1 背景簡介

1.1 RSML-e

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

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

1.2 NuSMV

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

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

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

2 形式化建模與驗證框架

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

圖1 形式化建模與驗證框架

2.1 RSML-e模型

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

圖2 RSML-e中的ANDOR

2.2 NuSMV的輸入與輸出

SMV程序由一個或多個模塊構(gòu)成，和C語言一樣，其中一個模塊必須稱為main，模塊可以聲明變量并賦值，程序最后給出要驗證的性質(zhì)，用CTL公式描述。如下給出了一段NuSMV程序的示例，包括主模塊和要驗證的性質(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 類型和變量的轉(zhuǎn)換

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

VAR identifier_name:var_type;

2.3.2 宏的轉(zhuǎn)換

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

2.3.3 相對時間概念

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

3 ASW具體實例

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

圖3 ASW抽象框架

針對ASW，運用RSML-e進(jìn)行建模。其中變量聲明部分應(yīng)包括輸入變量高度的數(shù)據(jù)變量、禁止信號的變量、重置信號的變量，以及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模型

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

MACRO when_inhibit_Pressed

Condition:

When(inhibit=ON);

MACRO when_ASW_Power_ON

Condition:

When(ASW=ON);

模型建立完成，接下來將模型轉(zhuǎn)換為NuSMV的輸入模型，根據(jù)第2節(jié)的變量轉(zhuǎn)換規(guī)則，對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()//主模式中的聲明部分

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

CTLSPEC

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

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

用NuSMV工具驗證得到的結(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

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

4 結(jié)束語

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

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

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

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

[4] 顧 斌,董云衛(wèi),王 政.面向航天嵌入式軟件的形式化建模方法[J].軟件學(xué)報,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] 楊 軍,葛海通,鄭飛君,等.一種形式化驗證方法:模型檢驗[J].浙江大學(xué)學(xué)報:理學(xué)版,2006,33(4):403-407.

[10] 呂 審.NuSMV模型檢測的研究及應(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] 鮑秋霜,張晉津.直覺主義計算樹邏輯中的安全性和活性[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ò)出版時間：2017-04-28

國家“973”重點基礎(chǔ)研究發(fā)展計劃項目(2014CB744900);航空科學(xué)基金(20150652008)

李 勇(1990-)，男，碩士生，研究方向為形式化方法;曹子寧，教授，博士生導(dǎo)師，研究方向為形式化方法、人工智能。

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