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

李 勇，曹子寧

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

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

李 勇，曹子寧

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

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

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

0 引 言

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

在形式化方法研究的基礎上，運用需求狀態機語言RSML-e對系統進行形式化需求規約，創建系統的形式化模型，在建模過程中能夠發現大量系統描述中的錯誤，而且能夠作為與用戶交互的實模型，并能夠以仿真的形式向客戶執行。但RSML-e不支持直接的模型檢測[6]。

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

1 背景簡介

1.1 RSML-e

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

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

1.2 NuSMV

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

CMU和IRST聯合開發的符號模型檢測工具NuSMV，用于檢測有限狀態系統是否滿足CTL約束公式。NuSMV是一種開放的模型檢測結構，它可以可靠地用于工業設計的驗證，執行過程為用戶將表示系統模型和約束規范的SMV程序作為輸入，NuSMV自動檢測約束規則在模型檢測中是否成立，若成立則輸出true，否則輸出false，并給出反例。

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

2 形式化建模與驗證框架

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

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

2.1 RSML-e模型

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

圖2 RSML-e中的ANDOR

2.2 NuSMV的輸入與輸出

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

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 轉換規則

2.3.1 類型和變量的轉換

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

VAR identifier_name:var_type;

2.3.2 宏的轉換

RSML-e中的宏對應轉換為NuSMV中的一個子模塊，可以做一一對應的轉換，RSML-e對應的參數應保持轉換，在NuSMV的子模塊添加參數，此外，子模塊必須在主模塊中添加聲明。

2.3.3 相對時間概念

RSML-e中用PREV的前綴表示當前研究狀態的前狀態，但NuSMV中只有next關鍵字表示后狀態，所以在做對應轉換時應將帶有PREV前綴的狀態描述為NuSMV中的當前狀態，而不帶前綴的描述為NuSMV中的后狀態，在后面的實例中加以說明。

3 ASW具體實例

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

圖3 ASW抽象框架

針對ASW，運用RSML-e進行建模。其中變量聲明部分應包括輸入變量高度的數據變量、禁止信號的變量、重置信號的變量，以及ASW的狀態變量，圖4給出高度變量和ASW狀態變量的RSML-e模型。

VARaltitude

Type:real

InitialValue:UNDEFINED

Classifiedas:MONITORED

狀態變量ASW：

STATE_VARIABLEASW

Type:{OFF,ON}

InitialValue:OFF

Classifiedas:State

圖4 高度變量和ASW狀態變量的RSML-e模型

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

MACRO when_inhibit_Pressed

Condition:

When(inhibit=ON);

MACRO when_ASW_Power_ON

Condition:

When(ASW=ON);

模型建立完成，接下來將模型轉換為NuSMV的輸入模型，根據第2節的變量轉換規則，對VAR關鍵字定義的變量可以轉換為：

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;

根據宏的形式化轉換規則，宏when_inhibit_Pressed轉換為：

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工具驗證得到的結果如下：

--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對示例中兩個邏輯公式驗證結果返回為true，表明建立的RSML模型滿足示例中的兩個屬性，否則會給出反例。后續可對更多的安全性和活性的屬性進行驗證。

4 結束語

將基于需求的形式化方法應用在航電領域，基于需求建模語言RSML-e對飛行導航系統進行建模，并用模型檢測器NuSMV對其進行形式化的模型轉換與驗證。具體實例的運行結果表明，所建立的模型滿足安全性和可靠性，能夠滿足航電的技術要求。后續研究可將需求建模、體系結構建模相結合，將形式化方法運用于系統開發的各個階段，從而給出從需求到驗證的一套完整的系統的形式化開發框架。

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

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

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

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

[5] 周玉平.基于UML-NuSMV模型的列控系統需求階段的安全分析[D].北京:北京交通大學,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].浙江大學學報:理學版,2006,33(4):403-407.

[10] 呂 審.NuSMV模型檢測的研究及應用[D].武漢:武漢理工大學,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].計算機科學與探索,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 網絡出版時間：2017-04-28

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

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

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