面向AltaRica模型的嵌入式系統安全性驗證方法*

仵志鵬，胡 軍,2+，陳 松，石嬌潔

1.南京航空航天大學 計算機科學與技術學院，南京 210016

2.南京大學 計算機軟件新技術國家重點實驗室，南京 210093

面向AltaRica模型的嵌入式系統安全性驗證方法*

仵志鵬1，胡 軍1,2+，陳 松1，石嬌潔1

1.南京航空航天大學 計算機科學與技術學院，南京 210016

2.南京大學 計算機軟件新技術國家重點實驗室，南京 210093

WU Zhipeng,HU Jun,CHEN Song,et al.Safety verification methodology of embedded system based on Alta-Rica model.Journal of Frontiers of Computer Science and Technology,2017,11(1)：24-36.

嵌入式系統；安全性驗證；AltaRica模型；Promela模型

1 引言

隨著嵌入式系統在航空、航天、能源動力、鐵路交通等領域的使用愈加廣泛，系統失效可能造成人員傷亡，財產損失，甚至環境危害等可怕后果。因此保證嵌入式系統的安全性和可靠性已然成為軟件工程領域研究的熱點問題之一[1]。為提高嵌入式系統的安全性和可靠性，針對系統模型的安全性分析與驗證已成為系統開發周期中的重要環節。

傳統的風險建模分析方法，如故障樹分析（fault tree analysis，FTA）[2]、失效模式影響分析（failure mode and effects analysis，FMEA）[3]、Markov Process[4]等在系統安全性分析中廣泛使用，但這些建模設計與系統規約形式之間還存在較大不同。AltaRica[5]建模語言可以較好地溝通系統規約形式與建模設計間的形式問題。隨著嵌入式系統的復雜度越來越高，嵌入式系統也變得多組件化。組件間交互以及依賴關系的設計成為嵌入式系統安全性分析的關注點，Alta-Rica模型的Dataflow[6]元素能夠很好地支持組件間的交互和組件間的依賴關系，同時組件間的依賴關系使用線性時序邏輯（line temporal logic，LTL）[7]進行規約。AltaRica模型結合LTL進行安全性驗證無法直接完成，但可以借助模型檢驗工具SPIN[8]來完成安全性驗證。SPIN是被廣泛使用的形式化驗證模型檢測工具，通過系統需求的LTL規約對系統模型窮盡分析完成嵌入式系統的安全性驗證。但SPIN并不能直接對AltaRica模型進行驗證，此時完成安全性驗證必須將AltaRica模型轉換成SPIN識別的輸入模型——Promela模型。

本文組織結構如下：第2章主要介紹AltaRica語法和Promela語法的形式化描述，并給出面向AltaRica模型的安全性驗證框架；第3章給出AltaRica模型到Promela模型[9]的轉換規則，并設計原型工具A2STool；第4章使用原型工具A2STool，以機輪剎車系統的機輪剎車控制單元子系統為例進行安全性驗證和分析；第5章介紹相關工作；第6章是總結與下一步工作。

2 AltaRica與Promela

為了準確地給出AltaRica模型到Promela模型的轉換規則，給出AltaRica語言語法的形式化描述和Promela語言的形式化描述，同時給出面向AltaRica模型的嵌入式系統安全性驗證的框架。

2.1 AltaRica的語義

結點node是AltaRica模型的基本組成部分，其他的語法元素都定義在node結點內。node結點根據是否含有子結點分為Equipment類型的結點和Component類型的結點。通用的node結點用九元組N表示，其中：

（1）E是結點中事件的集合；

（2）S是狀態變量的集合；

（3）F=FI?FO是流變量的集合，FI、FO分別為輸入流變量和輸出流變量，且FI?FO=?；

（4）I(S)是初始狀態;

（5）T(S,FI,ΓE,S′)是轉換公式，其中ΓE表示當前事件E發生，其中dom(ΓE)=E；

（6）P:FO→Expr(S)是狀態變量表達式與輸出變量的映射；

（7）對于?i=1,2,…,n，九元組N中的，當m≥0時，N中包含零個或多個AltaRica結點；

（8）A(F,N1.F1,N2.F2,…,Nn.Fn)表示流變量不變式的斷言區（Ni.Fi是子結點Ni所有流變量的集合）；

（9）V表示兩個及以上事件之間的同步關系。

針對九元組N：當S=?,I=True,T=True且對于任意的f∈FO有P(f)=True，N為Equipment類型；當n=0,A=True且V=?，N為Component類型。

2.2 Promela的語義

Promela是針對并發系統的建模語言，Promela模型作為成熟的模型檢驗工具SPIN的輸入模型，與SPIN共同完成并發系統的仿真和形式化驗證。Promela語言的許多標記從C程序語言中衍化出來，包括布爾語法、算子操作、賦值、等價、變量、參數定義、初始化變量、注釋以及指示程序塊開始和結束的花括號。Promela模型主要由proctype進程實體組成，一個Promela模型至少包含一個proctype定義，同時也必須要有一個proctype實例。proctype結構體內包含數據定義、其他聲明等。

Promela模型中通用的proctype用六元組P表示，其中：

（1）S表示狀態集合；

（2）S0∈S表示起始狀態；

（3）L是標記的集合，此標記可以是事件或者是要求滿足的某種條件；

（4）T?(S×L×S)是轉移的集合；

（6）F?S是終止狀態的集合。

2.3 面向AltaRica模型的系統安全性驗證框架

面向AltaRica模型的系統安全性驗證框架主要包含兩方面工作：一方面，通過系統需求對系統組件進行劃分，并將其與AltaRica模型元素進行映射，得到系統對應的AltaRica模型以及安全性需求的LTL規約；另一方面，將系統的AltaRica模型利用轉換規則轉換到Promela模型，結合模型檢測工具SPIN進行安全性驗證和分析。具體的安全性驗證框架如圖1所示。

Fig.1 Framework of safety verification forAltaRica model圖1 面向AltaRica模型的安全性驗證框架

3 AltaRica模型到Promela模型的轉換

SPIN是基于形式化方法的模型檢測工具，能夠對系統性質進行嚴格的窮盡分析。AltaRica模型能很好地支持系統組件間的交互和組件內的信息傳遞，特別適合當前多組件系統的建模。因此，針對嵌入式系統的安全性驗證可以利用AltaRica模型和SPIN的各自優勢，但SPIN并不能直接操作AltaRica模型。使用模型檢測工具SPIN需要將AltaRica模型轉換為SPIN接受的處理對象——Promela模型，從而完成系統的安全性驗證和分析。本節將具體介紹Alta-Rica模型到Promela模型的轉換規則和轉換規則的證明，以及轉換驗證工具A2STool的設計。

3.1 轉換規則

為便于轉換規則的精確定義，首先給出以下定義：A表示AltaRica模型，P表示Promela模型。

（1）結點node的轉換

AltaRica模型的node元素和sub元素一方面表示系統組件間的層次關系，另一方面兩者都是node結點聲明。系統組件在AltaRica模型中映射為結點，系統組件在Promela模型中映射為proctype進程實體，因此AltaRica模型結點轉換為proctype元素。精確定義為：N表示AltaRica模型的node結點，sub表示子結點；P表示Promela模型的proctype。因此Alta-Rica模型結點到Promela模型之間的轉換規則表示為：AN?PP&Asub?PP。轉換示例如圖2所示。

（2）流變量flow的轉換

AltaRica模型的flow元素完成系統組件間和組件內的信息傳遞，組件內信息傳遞由flow變量和狀態變量完成，組件間信息傳遞由關聯組件的flow變量通過assert元素來完成。

Fig.2 Transform example of node圖2 結點的轉換示例

①組件內信息傳遞flow變量的值與狀態變量的變化有關，然后通過assert完成綁定，狀態變量使用init聲明初始化。精確定義為：f和i為AltaRica模型結點flow聲明和init聲明，State和S0分別為Promela模型中的狀態變量和狀態初始化。組件內flow聲明的轉換規則表示為：。轉換示例如圖3所示。

Fig.3 Transform example of flow and init variable圖3 flow變量和init的轉換示例

②組件間flow變量表示組件間信息的傳遞，一般在相關組件的上層組件定義組件間的flow變量，而且flow變量的綁定通過assert聲明完成。精確定義：f為AltaRica模型中組件間的flow變量，State表示Promela模型中的狀態變量。flow聲明的轉換規則表示為：Af?PState。轉換示例如圖4所示。

Fig.4 Transform example of flow variable圖4 flow變量的轉換示例

（3）轉換trans的轉換

AltaRica模型的trans聲明和Promela模型狀態轉移都是系統狀態滿足一定的條件或在事件的影響下完成。精確定義：T表示AltaRica模型中trans聲明，Trans表示Promela模型轉換表達式中的狀態遷移。因此trans聲明的轉換規則為：AT?PTrans。轉換示例如圖5所示。

Fig.5 Transform example of trans variable圖5 trans變量的轉換規則

（4）事件event的轉換

AltaRica模型的event元素不僅影響組件內狀態的遷移，還影響到組件內flow變量以及相關聯組件。Promela模型可以使用枚舉類型mtype枚舉事件，然后定義mtype類型的事件變量Estate表示各個事件。精確定義：E代表AltaRica模型中的event變量，L代表Promela模型的標記。event元素對應的轉換規則表示為：AE?PL。轉換示例如圖6所示。

Fig.6 Transform example of event variable圖6 event變量的轉換示例

（5）同步sync的轉換

AltaRica模型的同步主要分為3類：強同步、弱同步、CCF同步。

強同步：AltaRica模型中強同步表示形式為sync。強同步具體語義：如果事件e1和e2的同步類型為強同步，則它們在組件c1和c2中對應的狀態遷移必須同時發生。Promela模型使用通道chan實現同步。精確定義：sync_strong表示AltaRica模型的強同步，chan表示Promela模型的同步聲明。因此強同步的轉換規則表示為：Async_strong?Pchan。轉換示例如圖7所示。

Fig.7 Transform example of Strong Synchronization圖7 Strong Synchronization的轉換示例

弱同步：AltaRica模型的弱同步是一種形如廣播的同步類型，形式為。弱同步的具體語義：若事件e1和e2同時發生，那么事件對應的轉換發生，否則事件e1(e2)發生且事件e2(e1)的守衛條件為true，e1和e2對應的轉換都會發生；事件e2(e1)的守衛條件為false，組件e2(e1)對應的轉換不發生。精確定義：sync_weak表示AltaRica模型的弱同步，chan表示Promela模型的同步聲明。轉換規則表示為：Async_weak?Pchan。弱同步對應的轉換示例如圖8所示。

Fig.8 Transform example of Weak Synchronization圖8 Weak Synchronization的轉換示例

CCF同步：CCF同步與弱同步很相似，在AltaRica模型中表示為。兩者的區別在于CCF同步的動機是為了描述由于內部錯誤或共同原因導致組件失效的情形。CCF同步用弱同步來表示，而內部錯誤和產生失效的共同原因e1、e2認為一個事件影響兩個組件的失效。

（6）常量和域的轉換

AltaRica模型除了結點node結構外，通常用const和domain關鍵字定義常量，Promela模型同樣在proctype外定義一些常量。針對domain，根據其表示的類型來具體轉換，如果是字符型，將其domain聲明映射為枚舉類型，否則定義為數值變量，同時對變量的值進行區間判斷。精確定義：c和d分別表示Alta-Rica模型的常量和域，int和m分別表示Promela模型的常量定義和枚舉類型mtypes。常量和域的轉換規則表示為：Ac?Pint,Ad?Pm。轉換示例如圖9所示。

Fig.9 Transform example of const and domain圖9 const和domain的轉換示例

以上給出了AltaRica模型到Promela模型的轉換規則和轉換示例，轉換規則總結如表1所示。

Table 1 Transform rules表1 轉換規則

上述轉換規則的操作對象是兩個模型的狀態、流變量、轉換、同步、事件等變量，因此并未增加變量，且模型轉換過程中的狀態空間也是線性增長，狀態空間與模型的結點和結點內的變量數決定。假設結點數為n，變量數目為m，那么所占用的狀態空間為n×m，且定義的轉換規則最終添加到AltaRica模型形成抽象語法樹。

3.2 轉換規則的正確性證明

由于AltaRica模型和Promela模型的實質是轉換系統，模型的語義也都是基于轉換系統的精確定義，需要對AltaRica模型和Promela模型進行語義分析。首先給出接口轉換系統的語義描述。

定義1（接口轉換系統）接口轉換系統[10]是一個六元組，其中：

（1）E是事件的集合，ε∈E；

（2）O是觀察者的集合；

（3）C是系統狀態的集合；

（4）I?C是初始狀態的集合；

（5）π:C→O每個配置（狀態）c∈C到觀察者的映射π(c)∈O；

（6）T是狀態轉移的集合，T∈C×E×C，如，其中c∈C。

接口轉換系統是基于包含觀察者O和映射函數π在內的標記轉換系統，也就是π定義了系統每一個稱為配置的狀態與O中觀察者的映射關系。觀察者表示的狀態集合可以被另一個接口轉換系統所看到，同時觀察者通常用來將組件內部狀態顯示給組件的上層組件，而AltaRica模型的層次結構是其特點之一。標記ε用來定義空事件，含有ε標記的轉換表示ITS中的配置（狀態）未發生改變。轉換暗含ITS的配置未發生改變，用來對異步建模，從而完成ITS間的同步機制。

2.1節和2.2節介紹了AltaRica模型和Promela模型的語義，接下來給出基于接口轉換系統兩模型的語義描述。

結點分為Equipment類型結點和Component類型結點，因此基于ITS定義結點的語義時也分為Equipment結點的ITS和Component結點的ITS。其中Component類型結點的ITSN定義為：

Equipment類型的結點，ITSN的配置集合C′和初始化狀態都是由子結點的配置和觀察者的結果組成，對于配置映射π′僅僅和觀察者配置相關。然而，轉換關系T″的定義很復雜，主要通過如下的步驟進行定義：首先，定義包含同步向量V的所有轉換的集合TC，其中局部事件的集合定義為VLOCAL，，同時定義W=Inst(v)×{v}，表示W為同步向量v與同步向量v對應實體笛卡爾積形成的對的集合。此時TC?C′×W′×C′包含所有的元素，同時對于所有,對于所有的。

然后，定義集合TB，其主要針對TC進行同步組件轉換的最大數進行約束，由此得到的TB轉換僅僅在和同步事件相關的組件內轉換活動。

最后，定義TA?C′×E′×C′約束ITSN的事件E′。滿足下面情況之一都有，同時T″=TA。

（1）當e∈E′且時，此時存在w=；

（2）存在c∈C′，滿足。

ITS很好地描述了AltaRcia模型的形式化語義，為了更好更精確地進行模型轉換，對于Promela模型使用ITS來描述Promela模型的語義。Promela模型進程實體定義為，則基于接口轉換系統的語義描述定義為ITSP，，具體的元素對應如下：

ITSP的事件和Promela模型的標記都表示發生狀態遷移所需滿足的條件或事件；ITSP的配置和ITSP的觀察者定義都為狀態變量的子集；ITSP中的初始值為Promela模型狀態的初始值；ITSP的配置到觀察者的映射表示系統狀態的子集與觀察者內配置的映射。ITSP的轉換T′不僅對應Promela模型的轉換Trans。

得到基于接口轉換系統的AltaRica模型和Promela模型的語義，接下來對3.1節提出的轉換規則進行證明。

AltaRica模型的結點N到Promela模型的進程P的轉換是正確的，因為基于接口轉換系統的ITSN和ITSP是同形異構的。

定理1如果N代表AltaRica模型的結點，P為轉換的目的模型Promela的進程實體，那么N基于接口轉換系統的定義和P基于接口轉換系統的定義等價。

關于AltaRica模型到Promela模型轉換的正確性證明：首先ITSN和ITSP的每一個配置都是雙射，即滿足接口轉換系統初始化和不變量配置的狀態集相同；然后，ITSN和ITSP的轉換也是雙射。通過以上存在配置和轉換兩個雙射函數就可以保證實現等價的轉換。完整的證明如下。

假設ITSN中每個配置c∈C和每個元組之間存在雙向映射關系，同樣Promela模型進程實體中每個狀態q∈CP和變量VP賦值函數μq之間也存在雙向映射關系。

此時，存在一個雙射函數ξ：CN→CP，對于給定的由元組定義的狀態c∈CN，得到ξ(c)=q，此時q=μq(VP)且μq由確定。定義ξ-1：Q→CN是QP到CN的反映射函數。

現在需要證明ITSN和ITSP的轉換關系等價，也就是說的充分必要條件是。

此外，存在3個不相交的集合分別是IdxWeak、IdxSync和Idxε，它們滿足如下性質：

（1）IdxWeak?IdxSync?Idxε={1,2,…,n}，IdxWeak?IdxSync=?，IdxWeak?Idxε=?且IdxSync?Idxε=?；

（1）ei=ε且ei′=ε。基于AltaRica的語義，不存在影響狀態q遷移的同步向量v2∈V，其中v2=。而且Promela對于空事件i.EVENT=ε的情況時，i不參加同步。

必要性：對于任意的狀態q,q′∈CP和任意的事件e∈EP，若q,e,q′∈TransP，則。假定s=ξ-1(q)，s′=ξ-1(q′)，如果，由ITSP的定義得到。完成必要性的證明要求證明存在轉換。e有3種可能的形式：

（3）e=v.ec，其中v∈VN，ec∈Inst(v)，基于AltaRica結點的接口轉換系統定義得到。此時，若v表示強同步則有；若v表示弱同步，由于，只有q不滿足弱同步的守衛條件時才能確保ei=s，因此e是v含有同步實體最多的同步向量，此時。因此TN中存在對應的轉換。

3.3 轉換工具的設計

根據上述基于AltaRica模型的嵌入式軟件安全性分析方法，設計了一款原型分析工具A2STool，其具體設計框架如圖10所示。

Fig.10 Design framework ofA2STool圖10 A2STool的設計框架

A2STool工具從系統設計出發，主要設計框架分為應用層、業務層和持久層，下面對各層進行說明。

應用層提供了AltaRica模型編輯器、模型轉換工具和模型驗證功能。

業務層除了接收應用層傳過來的操作指令進行業務處理，同時還需要應用層提供AltaRica模型文件和待驗證屬性。AltaRica模型文件作為整個工具的輸入，首先對其使用語法分析工具ANTLR[11]進行語法分析得到語法分析樹；然后語法分析樹和轉換規則結合起來得到目標模型Promela模型文件；最后Promela模型作為驗證工具SPIN的輸入完成應用層驗證功能。

持久層對用戶使用過程產生的數據進行管理，例如存取AltaRica模型和轉換形成的Promela模型。原型工具的處理流程如圖11所示。

Fig.11 Processing flow ofA2STool圖11 A2STool的處理流程

上述的處理流程主要分為3個步驟：

（1）A2STool工具的輸入過程。主要包括系統設計的AltaRica模型和系統安全性需求的LTL規約。其中AltaRica模型作為直接輸入，而安全性需求的LTL規約則用于安全性驗證階段。

（2）A2STool工具的模型轉換過程。主要包括語法分析工具ANTLR對AltaRica模型進行語法檢查，生成抽象語法樹，結合轉換規則生成Promela模型。這個轉換過程首先需要AltaRica模型的文法文件，圖12給出了AltaRica語言的部分文法。轉換過程得到的Promela模型作為模型檢驗工具SPIN的輸入。

Fig.12 Part syntax file ofAltaRica language圖12 AltaRica語言的文法文件

（3）A2STool工具的驗證過程。主要包括模型檢驗工具SPIN對Promela模型結合安全新需求的LTL規約進行窮盡分析，并完成安全性驗證工作。

A2STool原型工具的顯示界面如圖13所示。

Fig.13 Important page ofA2STool圖13 A2STool的主要頁面

4 實例分析

本文利用設計的工具對航電系統的機輪剎車系統[12]的控制單元進行安全性驗證。首先根據該系統的描述建立起對應的AltaRica模型；然后檢查建立的模型語法；接著將AltaRica模型轉換到Promela模型；最后通過模型檢測工具SPIN對包含安全性需求LTL規約的Promela模型進行安全性驗證，并分析驗證結果。

4.1 系統描述

機輪剎車系統（wheel brake system，WBS）包含一個數據控制單元，即剎車系統控制單元（brake system control unit，BSCU）以及兩個液壓線路，即正常線路（由綠色液壓泵提供液壓值，也可稱為綠液壓系統）和備用線路（由藍色液壓泵或者蓄壓泵提供液壓值，也可稱為藍液壓系統）。系統從外部環境中讀入自動剎車、減速率、飛機速度和打滑的數值信息作為輸入。這些數據輸入到BSCU中，經過計算產生剎車命令。機輪剎車系統的控制結構如圖14所示。

Fig.14 Control unit of wheel brake system圖14 機輪剎車系統控制單元

剎車系統控制單元是整個機輪剎車系統中唯一的數據組件。其輸入大都來自于更高級別的WBS，位于正常線路和備用線路不同位置上的一些反饋值同時作為本身的輸入，而且同時擁有兩個獨立的電源供應。BSCU由兩個子系統構成，兩個子系統各自有一個電源進行供應，每個子系統包含有一套命令單元和監控單元。命令單元產生正常命令和備用命令，分別作用于正常線路和備用線路。監控單元主要用于監控對應的命令單元產生的命令是否有效，若兩個命令單元均有效，則BSCU有效，并默認使用第一個命令單元的命令；若兩個命令單元中只有一個命令是有效的，則BSCU有效，且使用該命令單元產生的命令；若兩個命令單元產生的命令均無效，則BSCU無效，兩個命令單元產生的命令均不可用。

將WBS的各個組件作為AltaRica模型中的結點，使用UML對BSCU進行描述，如圖15所示，該BSCU子系統對應的部分AltaRica模型代碼如圖16所示。

Fig.15 UML class diagram of BSCU圖15 BSCU的UML類圖表示

Fig.16 Part code of BSCUAltaRica model圖16 BSCU的部分AltaRica模型

4.2 模型轉換和驗證分析

將4.1節得到的剎車系統控制單元的AltaRica模型導入A2STool工具，依次完成語法檢查和模型轉換操作，轉換后的Promela模型如圖17所示。

要保證整個WBS的安全性，首先必須保證BSCU正常工作，由系統需求出發得到如下安全性需求：

Fig.17 Part code of transformed Promela model byA2STool圖17 A2STool轉換后的部分Promela模型

（1）電源正常（PowerOn=true）工作的情況下，不允許出現BSCU失效（IsBSCU=false）的情況。該安全性需求的LTL規約表示：ltl ss{[]((PowerOn==true) -＞＜＞(IsBSCU==true))}。在A2PSTool工具集成的模型檢測工具SPIN的驗證結果如圖18所示。

Fig.18 Verification result ofA2STool圖18 A2STool下的驗證結果

（2）電源正常（PowerOn=true），同時命令單元1產生正常命令（NorCommand=true）的情況下，不允許出現BSCU失效（IsBSCU=false）的情況。該安全性需求的LTL規約表示：ltl ss{[](((PowerOn==true) (NorCommand==true))-＞＜＞(IsBSCU==true))}。在A2STool工具集成的模型檢測工具SPIN的驗證結果如圖19所示。

（1）（2）兩個安全性需求驗證的結果表明：當前的BSCU設計未考慮如上的兩種安全性需求，需重新對BSCU子系統進行設計。本文提出了一套理論方法，對系統安全性設計進行驗證，且同類工作較少，只有文獻[13]的工作是對AltaRica轉換到NuSMV進行驗證，采用標記模型檢測的方式。而本文采用窮舉驗證。該實驗證明了本文設計的轉換規則的正確性，提出了一種解決系統安全性驗證的新思路。

Fig.19 Verification result ofA2STool圖19 A2STool下的驗證結果

5 相關工作

工業界和學術界為了提高安全關鍵領域嵌入式系統的安全性，系統安全性分析成為系統開發周期中的重要環節。AltaRica作為一種形式化的建模語言，已有很多學者與工業界研究人員在用其進行系統建模以及基于AltaRica進行安全性分析。文獻[14]介紹了AirBus和ONERA使用形式化建模語言Alta-Rica及其相應工具對電氣和液壓系統進行安全性分析的工作。文獻[15]介紹了兩種經典的模型檢驗工具SPIN和NuSMV，制定了SPIN到NuSMV模型的轉換規則，實現了SPIN到NuSMV輸入模型的自動轉換。文獻[13]介紹了AltaRica模型到HyDI語言的轉換，進而使用模型檢測工具NuSMV進行安全性評估分析，并對AltaRica模型到HyDI語言的轉換進行了證明。文獻[16]介紹了在規模和復雜度提高的情況下AltaRica建模方法，解決了建立完整、精確和一致安全模型的困難，對液壓系統使用AltaRica進行建模，并進行了安全性分析。文獻[17]依據直升機渦輪引擎提出了從初步系統安全性評估分析中推導出軟件功能需求的方法。該方法使用AltaRica模型和相應工具從系統失效傳播模型中抽取功能失效路徑；然后分析此路徑得到功能軟件需求的最小組合。文獻[6]通過風險分析和功能分析來構建AltaRica數據流模型，同時找到SysML與AltaRica數據流模型對應的元素映射。文獻[18]使用形式化建模語言Alta-Rica和相應的工具交互仿真系統內部失效的傳播，然后通過模型檢驗驗證定性需求以及建立故障樹分析產生描述失效事件的序列。文獻[19]使用AltaRica語言對空客A320飛機液壓系統進行建模，同時展示怎樣單獨使用故障樹生成和模型檢測，進而結合二者評估安全需求。與已有工作相比，本文主要從AltaRica模型出發，采用語法分析工具ANTLR對其進行解析得到抽象語法樹，最后結合抽象語法樹和定義轉換規則完成模型轉換得到Promela模型。采用模型檢驗工具SPIN對Promela模型和相應的安全需求的LTL規約進行安全性驗證。

6 總結及進一步工作

本文提出了一種采用模型轉換和模型驗證對嵌入式系統進行安全性驗證的方法。同時設計了一款集AltaRica模型編輯功能、模型轉換功能、模型驗證功能的工具A2STool。首先，將嵌入式系統利用AltaRica建模語言進行建模得到AltaRica模型；其次，使用語法分析工具ANTLR對模型進行解析得到語法樹，將其與轉換規則結合進行模型轉換得到Promela模型；最后，基于Promela模型使用模型檢驗工具SPIN對安全性需求LTL規約進行驗證。通過模型驗證找出系統設計的安全性問題，及時進行系統設計調整，提高系統的安全性。

未來的進一步工作主要包括以下兩方面：（1）本文給出的轉換規則并未包含AltaRica語言的所有元素，將對其他元素的轉換規則繼續進行研究；（2）將對AltaRica在時間上的擴展作為下一步的研究重點之一。

[1]Huang Zhiqiu,Xu Bingfeng,Kan Shuanglong,et al.Survey on embedded software safety analysis standards,methods and tools for airborne system[J].Journal of Software,2014, 25(2):200-218.

[2]Xu Bingfeng,Huang Zhiqiu,Hu Jun,et al.Time property analysis method for state/event fault tree[J].Journal of Software,2015,26(2):427-446.

[3]Medikonda B S,Ramaiah P S,Gokhale A A.FMEA and fault tree based software safety analysis of a railroad crossing critical system[J].Global Journal of Computer Science andTechnology,2011,11(8):57-58.

[4]Zhou Guochang,Guo Baolong,Gao Xiang,et al.Research on the system reliability modeling based on Markov process and reliability block diagram[C]//Proceedings of the 1st Euro-China Conference on Intelligent Data Analysis and Applications,Shenzhen,China,Jun 13-15,2014.[S.L]:Springer International Publishing,2014:545-553.

[5]Griffault A,Lajeunesse S,Point G,et al.The AltaRica language[C]//Proceedings of the 1998 International Conference on Safety and Reliability,1998:20-24.

[6]David P,Idasiak V,Kratz F.Automating the synthesis ofAlta-Rica data-flow models from SysML[M]//Reliability,Risk and Safety:Theory and Applications.London:Taylor& Francis Group,2009:105-112.

[7]Pnueli A.The temporal logic of programs[C]//Proceedings of the 18th Annual Symposium on Foundations of Computer Science,1977:46-57.

[8]Clarke E M,Grumberg O,Peled D.Model checking[M]. Cambridge,USA:MIT press,1999.

[9]Inverardi P,Muccini H,Pelliccione P.Automated check of architectural models consistency using SPIN[C]//Proceedings of the 16th Annual International Conference on Automated Software Engineering,San Diego,USA,Nov 26-29,2001. Piscataway,USA:IEEE,2001:346-349.

[10]Parr T J,Quong R W.ANTLR:a predicated-LL(k)parser generator[J].Software:Practice and Experience,1995,25 (7):789-810.

[11]Arnold A,Point G,Griffault A,et al.The AltaRica formalism for describing concurrent systems[J].Fundamenta Informaticae,1999,40(2/3):109-124.

[12]Joshi A,Heimdahl M P E,Miller S P,et al.Model-based safety analysis[R].Contractor Report Cecilia Haskins,Nasa Langley Research Center,2006.

[13]Bozzano M,Cimatti A,Lisagor O,et al.Safety assessment of AltaRica models via symbolic model checking[J].Science of Computer Programming,2015,98:464-483.

[14]Bieber P,Bougnol C,Castel C,et al.Safety assessment with Altarica[C]//Building the Information Society:IFIP 18th World Computer Congress Topical Sessions,Toulouse, France,Aug 22-27,2004.[S.l.]:Springer US,2004:505-510.

[15]Jiang Yong,Qiu Zongyan.S2N:model transformation from SPIN to NuSMV[C]//LNCS 7385:Proceedings of the 19th International Workshop on Model Checking of Software, Oxford,UK,Jul 23-24,2012.Berlin,Heidelberg:Springer, 2012:255-260.

[16]Li Shaojun,Duo Su.A practicable MBSA modeling process using AltaRica[C]//LNCS 8822:Proceedings of the 4th International Symposium on Model-Based Safety and Assessment,Munich,Germany,Oct 27-29,2014.[S.l.]:Springer International Publishing,2014:1-13.

[17]Humbert S,Seguin C,Castel C,et al.Deriving safety software requirements from an AltaRica system model[C]// LNCS 5219:Proceedings of the 27th International Conference on Computer Safety,Reliability,and Security,Newcastle upon Tyne,UK,Sep 22-25,2008.Berlin,Heidelberg: Springer,2008:320-331.

[18]Zhu Yuanzhen,Zhang Jianguo,Gong Qi,et al.Reliability and safety assessment with AltaRica for complex aircraft systems[C]//Proceedings of the 2011 9th International Conference on Reliability,Maintainability and Safety,Guiyang, China,Jun 12-15,2011.Piscataway,USA:IEEE,2011:588-593.

[19]Bieber P,Castel C,Seguin C.Combination of fault tree analysis and model checking for safety assessment of complex system[C]//LNCS 2485:Proceedings of the 4th European Dependable Computing Conference,Toulouse,France, Oct 23-25,2002.Berlin,Heidelberg:Springer,2002:19-31.

附中文參考文獻：

[1]黃志球,徐丙鳳,闞雙龍,等.嵌入式機載軟件安全性分析標準、方法及工具研究綜述[J].軟件學報,2014,25(2): 200-218.

[2]徐丙鳳,黃志球,胡軍,等.一種狀態事件故障樹的時間特性分析方法[J].軟件學報,2015,26(2):427-446.

WU Zhipeng was born in 1989.He is an M.S.candidate at Nanjing University of Aeronautics and Astronautics.His research interests include software safety analysis and model checking,etc.

仵志鵬（1989—），男，河南周口人，南京航空航天大學碩士研究生，主要研究領域為軟件安全性分析，模型檢測等。

HU Jun was born in 1973.He received the Ph.D.degree in computer software and theory from Nanjing University in 2006.Now he is an associate professor at Nanjing University of Aeronautics and Astronautics,and the member of CCF.His research interests include model-based safety analysis,software verification and embedded system design,etc.

胡軍（1973—），男，湖北黃岡人，2006年于南京大學計算機軟件與理論專業獲得博士學位，現為南京航空航天大學計算機科學與技術學院副教授，CCF會員，主要研究領域為模型驅動的系統安全性分析，軟件驗證，嵌入式系統設計等。主持過航空基金、教育部博士點基金、國防預研基金、教育部留學人員啟動基金、南京航空航天大學科技創新基金等項目，并參與多項國家自然科學基金、國防預研以及863計劃等項目。

CHEN Song was born in 1991.He is an M.S.candidate at Nanjing University of Aeronautics and Astronautics.His research interests include software safety analysis and model checking,etc.

陳松（1991—），男，山東泰安人，南京航空航天大學碩士研究生，主要研究領域為軟件安全性分析，模型檢測等。

SHI Jiaojie was born in 1990.She is an M.S.candidate at Nanjing University of Aeronautics and Astronautics.Her research interests include software safety analysis and model checking,etc.

石嬌潔（1990—），女，河南鄭州人，南京航空航天大學碩士研究生，主要研究領域為軟件安全性分析，模型檢測等。

Safety Verification Methodology of Embedded System Based onAltaRica Model*

WU Zhipeng1,HU Jun1,2+,CHEN Song1,SHI Jiaojie1
1.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China
2.State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China
+Corresponding author:E-mail:wuzhipeng2013@nuaa.edu.cn

As the embedded system is widely used in the safety-critical fields such as aeronautics,astronautics and transportation,AltaRica is a kind of formal modeling languages for safety-critical systems.Modeling critical systems based on AltaRica model and the safety analysis upon this have become the industrial standard in Europe.This paper proposes a kind of embedded system safety verification method based on AltaRica model,which includes, firstly model the embedded system using AltaRica,then exhibit the transformation rules from AltaRica model to Promela model,at the same time do formal proofs on transformation rules,so as to acquire the Promela model of embedded system,and finally use SPIN,a model check tool,to analyze and verify it.This paper takes the control unit of wheel brake system as an example to verify this transformation rules and method.

embedded system;safety verification;AltaRica model;Promela model

A

：TP311.5

10.3778/j.issn.1673-9418.1511003

*The National Basic Research Program of China under Grant No.2014CB744903(國家重點基礎研究發展計劃(973計劃));the Scientific Research Foundation for the Returned Overseas Chinese Scholars,State Education Ministry of China under Grant No.2012(教育部回國留學人員科研啟動基金);the Science Foundation for Youth Science and Technology Innovation of Nanjing University of Aeronautics andAstronautics under Grant No.NS2014098(南京航空航天大學青年科技創新基金).

Received 2015-11,Accepted 2016-02.

CNKI網絡優先出版:2016-02-19,http://www.cnki.net/kcms/detail/11.5602.TP.20160219.1651.002.html

摘 要：嵌入式系統在航空、航天、交通等安全關鍵領域的使用愈加廣泛，AltaRica是一種描述安全關鍵系統的建模語言，同時基于AltaRica模型的安全性分析已成為歐洲的工業標準。提出了一種面向AltaRica模型的嵌入式系統安全性驗證方法，包括：使用AltaRica語言對嵌入式系統進行建模；給出AltaRica模型到Promela模型的轉換規則；對轉換規則進行形式化證明，得到嵌入式系統的Promela模型；使用模型檢驗工具SPIN進行安全性驗證。通過機輪剎車系統中的機輪剎車控制單元進行實例分析，驗證了轉換規則的正確性和有效性。