模型驅動的嵌入式系統設計安全性驗證方法研究*

劉 雪，胡 軍，2，黃志球，馬金晶，程 楨，石嬌潔

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

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

模型驅動的嵌入式系統設計安全性驗證方法研究*

劉 雪1，胡 軍1，2，黃志球1，馬金晶1，程 楨1，石嬌潔1

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

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

基于模型的嵌入式系統安全性分析與驗證方法是近年來在安全攸關系統工程領域中出現的一個重要研究熱點。提出一種基于模型驅動架構的面向Sys ML/MARTE狀態機的系統安全性驗證方法，具體包括：構建了具備Sys ML/MARTE擴展語義的狀態機元模型，以及安全性建模與分析語言AltaRica的語義模型GTS的元模型；然后建立了從Sys ML/MARTE狀態機模型分別到時間自動機模型以及AltaRica模型的語義映射模型轉換規則，并基于AMMA平臺和時間自動機驗證工具UPPAAL設計實現了對Sys ML/MARTE狀態機的模型轉換與系統安全性形式化驗證的框架。最后給出了一個飛機著陸控制系統設計模型的安全性驗證實例分析。

系統安全性分析；模型驅動工程；Sys ML/MARTE；狀態機模型；嵌入式系統

1 引言

模型驅動工程MDE（Model Driven Engineering）［1～3］是近十年來在系統工程 以及軟件工程領域中出現的主流方法，其基本思想是以系統模型設計、模型轉換與分析/驗證為工程的重要核心，提高對復雜工程系統開發與維護的能力和效率。與此同時，建立基于模型的系統安全性分析方法并結合形式化方法進行驗證也逐漸成為嵌入式安全攸關系統開發過程中的需求和重要挑戰，如：在2013年版本的機載軟件安全性適航標準DO-178C中已經正式提出了基于模型的系統開發和形式化方法分析 的要求［4］。

傳統的嵌入式系統設計與開發中是由安全工程師來直接構造故障樹、馬爾科夫鏈等進行系統安全性分析，不足以應對近年來規模和復雜度迅速增長的嵌入式安全攸關系統的設計開發與升級維護的要求，需要在系統設計開發過程中盡可能采用統一的模型形式，建立有效的系統模型轉換方法并結合形式化分析技術來提高系統安全性分析的效率［5，6］。Sys ML（System Modeling Language）［7］是目前系統工程應用開發的標準建模語言規范，支持包括對復雜嵌入式系統進行規約、設計和分析。MARTE（Modeling and Analysis of Real-Time Embedded systems）［8］主要提供了嵌入式系統中的時間約束、資源分配等非功能屬性的建模與分析。通常這兩者結合起來可以有效描述嵌入式實時系統的功能行為。AltaRica［9］是一個以衛式轉換系統為語義基礎進行系統安全行為建模與分析的語言及工具，已在航空電子設備系統架構安全評估 中得到 應 用［10］。

本文的主要研究工作是在 MDE架構下以Sys ML模型中的狀態機模型作為核心研究對象，結合MARTE中的時間、資源等方面語義擴展，用以對復雜嵌入式實時系統的行為建模；然后分別建立從Sys ML/MARTE狀態機模型到AltaRica模型的轉換和Sys ML/MARTE狀態機模型到時間自動機模型的轉換方法，并在AMMA（ATLAS Model Management Architecture）［11］平臺上進行了包括語法/語義的模型轉換的具體實現。前者的轉換使我們能在AltaRica模型中獲取安全性分析所需要的故障樹以及相應的時序邏輯公式；后者的轉換使得可以采用形式化分析工具UPPAAL來展開系統行為設計的安全性驗證。

具體內容安排如 下：第 2節概 要介紹了Sys ML及MARTE模型，并針對Sys ML中的狀態機模型，給出了在本文工作中所構造的結合MARTE語義信息的擴展狀態機的元模型；第3節主要介紹了AltaRica安全性建模語言及其形式化描述GTS模型；第4節給出了本文所提出的基于模型轉換的安全性驗證框架，包括從Sys ML/ MARTE狀態機模型到GTS模型的轉換方法、從Sys ML/MARTE狀態機模型到時間自動機模型的轉換方法以及基于UPPAAL工具的系統設計安全性驗證過程；第5節在前述模型轉換方法的基礎上實現了一個基于AMMA的模型轉換與驗證平臺，并給出了實例分析；最后是相關研究工作和總結。

2 Sys ML/MARTE模型

本節主要介紹系統建模語言 Sys ML和MARTE模型，并針對Sys ML中的狀態機模型，給出了在本文工作中所構造的結合MARTE語義信息的擴展狀態機的元模型，為后面工作提供模型轉換與驗證的基礎。

2.1 Sys ML與MARTE概述

Sys ML是面向系統工程領域并在UML 2.0的基礎上進行重用和擴展所得到建模語言，彌補了UML在系統工程領域建模的缺陷，已經成為工業界在系統工程設計與分析過程中的標準建模語言。Sys ML的主要目的是支持在各種復雜系統開發中進行詳細規約說明、系統設計、分析與驗證等重要過程，因此Sys ML一方面重用了UML中典型的建模元素包，同時使用擴展機制（包括模型元素的定義類型、元類和模型庫）對UML中的活動包、類包和輔助包等增加了一些新的語法語義；另一方面還增加了一些 UML沒有的新包，如需求包、參數包和分配包［7］。Sys ML建模語言具有的包括硬軟件在內系統級信息的特征，使其比較適合應用于現代復雜嵌入式系統領域中的設計與分析研究［7］。

在實時與嵌入式系統領域中進行建模與分析還存在另外一個建模規范MARTE［8］。MARTE是專門針對UML以及Sys ML中尚缺乏對嵌入式系統中所特別關注的各類系統非功能屬性進行準確描述的能力而進行的擴展，其包含了相當豐富的系統非功能屬性建模元素（如：時間、資源、可靠性、安全性、調度等）。圖1中給出了MARTE規范中建模元素包的總體架構。

Figure 1 Package structure of the MARTE圖1 MARTE建模元素包的總體結構圖

MARTE中建模元素總共分為四個部分：基礎包、設計模型包、分析模型包和附件包。其中，基礎模型包給出了實時和嵌入式系統中的一些核心概念模型，如優先級、響應時間、執行周期、受限資源等，這些概念是構建系統設計和分析模型的基礎。設計模型包中則提供了較高抽象層的建模元素，用于對并發和實時的活動主體和行為進行建模。分析模型包則包含用于對系統的性能和可靠性等進行分析的模型元素。由于 MARTE中具備上述特征，因此我們可以在復雜嵌入式實時系統設計領域中綜合采用Sys ML與MARTE的建模能力，并進一步建立相應的分析方法。

2.2 SysML/MARTE的狀態機及其元模型構造

狀態機（State Machine）是Sys ML中對系統動態行為進行建模的重要模型圖之一，它能方便清晰地描述系統動態行為變化。StateMachine包中定義了很多通過有限狀態遷移系統對離散行為模型

建模的概念，包括初始狀態、終止狀態、簡單狀態、觸發事件、衛式、遷移和區域等。圖2為一個簡單計數功能的Sys ML狀態機示例。但是，在典型的Sys ML狀態機模型中還缺少資源、時間等方面的非功能屬性的完整表達，如：在狀態機模型中只是提供了一個簡單的時間計時方式等，還不足以用來表達嵌入式實時系統建模分析所需的時間特征。因此，在對復雜嵌入式實時系統建模中，我們還需要結合MARTE中的相關模型元素的語義進行擴展。

在本文工作中首先主要是采用MARTE中有關時間方面的建模元素來對Sys ML中的狀態機模型進行擴展，并進一步構建其相應的元模型。由于MARTE自身的擴展機制是基于增加模型元素的注釋來實現的，因此，我們可以采用同樣的增加狀態機模型中的注釋的形式來進行擴展并建立元模型。MARTE中的時間建模由時間基、多時間基、時間點和時間結構關系構成。MARTE中的時鐘（Clock）是用來訪問時間結構的模型元素，可以將狀態機中具體的狀態、動作、事件或衛式約束關聯到時鐘實例。MARTE時鐘包里面提供了邏輯時間和計時時間，邏輯時間是通過事件發生的次數來定義，計時時間（Chronometric Time）用來描述物理時間；可以處理系統對不同時鐘的需求，并能描述系統行為依賴多個時鐘以及對系統時間約束的問題［12］，為系統提供計時時間以及對系統時間進行約束。考慮到面向復雜嵌入式實時系統設計中對實時性要求，本文采用了MARTE時間中計時時間的模型語義來擴展狀態機。

Figure 2 Sys ML state machine diagram of the counting function圖2 計數功能的Sys ML狀態機示例

以下給出本文基于SysML規范中狀態機中模型元素的定義以及MARTE中時間相關建模元素的分析所構建的Sys ML/MARTE擴展形式的狀態機元模型（見圖3）。這個元模型圖邏輯上可分為兩個部分，其一是SysML中的狀態機元模型，其中狀態機（StateMachine：Sm）由頂點（Vertex）、轉換（Transition）和參數（Parameter）三部分組成。區域類（Region）包含狀態機所有的狀態、狀態分組以及狀態屬性，本文將MARTE中的時鐘附加到狀態機元模型的Region的屬性On中，這樣就能在Sys ML狀態機任何一個元素上添加時鐘約束信息。Exponentialrate、isBranch Point和prob都是和概率相關的元素。Exponentialrate是一個概率表達式，它指明了指數概率分布。isBranch Point用于指明一個狀態是否為概率分支。prob指明了遷移可能觸發的概率。變遷有一定的約束條件，變遷發生會觸發一些動作，還會發生一些行為，狀態可以定義不變式，說明狀態的約束條件。另一部分是MARTE中的時間相關的元模型，其中Clock代表訪問時間，Timed Element是所用計時概念的抽象，將時間元素與非空Clock集聯系在一起；Timed Event、Timed Message和TimedProcessing分別表示有時間約束的事件（定期時鐘節拍）、消息或活動等；Timed Instant Observation和Timed Duration Obervation則用來表示時鐘值或時間間隔，TimedInstantConstraint和TimedDurationConstraint則可以用來表示與時間相關的約束等。

3 AltaRica模型

基于模型的安全性分析（Model-based Safety Analysis）是近年來在實時嵌入式系統工程領域出現的重要研究方向［13］，其基本思想是在系統設計過程中進行系統安全性分析的時候，首先建立包括系統功能行為和故障行為的模型，然后基于模型展開安全性分析與驗證，如：構造典型可靠性分析所使用的故障樹以及馬爾科夫鏈模型做安全性分析，或者結合形式化驗證工具進行驗證等。AltaRica［14］就是一種基于形式化的衛式轉換（Guarded Transition System）的安全性建模語言，可以用來對復雜安全攸關系統進行建模分析。

AltaRica模型可以分為語法和語義兩個層面。

語法層面的表示形式是將系統建模為具備層次結構的節點（Node）集合，每個節點具有多個狀態、事件、轉換、輸入/輸出、數據變量等特征，其具體的行為使用類似于自動機的形式來表達。如圖4中所給出的AltaRica中一個節點組件的模型示例，它描述了節點具有工作、維修和失效三種狀態；當組件處在工作狀態時如果發生failure事件，那么組件會轉移到失效狀態；其他遷移按照同樣方式進行。

Figure 4 Example of the AltaRica model圖4 AltaRica模型示例

AltaRica在語義層面上是一個衛式轉換系統GTS的形式化模型［15］，其嚴格的定義為一個五元組，其中：（1）V是一組變量，為一組狀態變量S和流變量E的正交并集；（2）E是一組事件；（3）T是一組轉換，每個轉換是一個三元組，其中e是E的一個事件，G是一個建立在變量V上的布爾表達式，P是一個建立在變量V上的操作。通常將轉換表示成e：G→P的形式。AltaRica的語法模型通過編譯轉換成相應的GTS模型，并可以生成系統故障樹模型，以及進一步構造相應的時序邏輯公式等后續分析工作。在文獻［14，16］中，分別給出了將GTS轉換成一組布爾公式（故樟樹）的方法，以及從故障樹模型構造時序邏輯公式的方法。

雖然AltaRica這種采用狀態/轉換的高層次模型形式來代替直接設計故障樹模型提高了系統工程中設計、共享和維護模型的效率，但是與工業界目前已經認可并使用的Sys ML/MARTE建模語言存在表示形式上較大的不同。因此，本文接下來的主要工作就是建立Sys ML/MARTE行為模型與AltaRica模型之間的語法語義映射關系，設計自動化的模型轉換方法，并利用AltaRica模型可以生成故障樹的特點，展開基于Sys ML/MARTE模型的系統安全性分析與驗證，使得在復雜嵌入式系統設計中只需要熟練掌握Sys ML/MARTE的建模即可，提高系統設計與分析的效率。

Figure 3 Meta-model of the Sys ML/MARTE state machine圖3 Sys ML/MARTE擴展形式的狀態機元模型

4 系統安全性驗證框架

本節中給出基于Sys ML/MARTE模型轉換的嵌入式系統設計的安全性驗證框架。首先給出了驗證框架中總體上模型轉換與驗證的過程說明，然后分別給出了從SysML/MARTE狀態機模型到GTS模型，以及時間自動機模型的轉換方法。

4.1 基于模型轉換的安全性驗證框架

模型驅動工程［17］是近十 年來在 系統 工程 以及軟件工程領域中出現的主流方法，其基本思想是以系統模型設計、模型轉換與分析/驗證為工程開發的重要核心，提高復雜工程系統開發與維護的能力和效率。圖5中給出了在MDE架構下本文所設計的基于SysML/MARTE模型轉換的嵌入式系統設計安全性質的形式化驗證框架。整個框架總體上可以分為三個部分，如下所述：

首先，我們使用擴展形式Sys ML/MARTE狀態機模型對嵌入式系統的故障行為進行建模，作為模型轉換的源模型；并與此同時構建擴展的狀態機元模型與GTS元模型之間的語義映射規則（其中GTS元模型的構造以及語義映射規則在4.2節中詳細給出）。這樣就可以通過 AMMA平臺［11］的模型轉換引擎將狀態機源模型自動轉換成GTS目標模型；然后通過AMMA平臺中的TCS［18］組件，在語法層面上將GTS目標模型轉換為AltaRica的文本模型。這樣就可以使用AltaRica工具來自動構造與系統故障行為相關的故障樹模型，并進一步生成系統行為應滿足的安全性質（可以用時序邏輯公式來表示）。

當獲得了系統行為所需滿足的安全性質后，為了能夠完成形式化驗證，還需要進一步構造系統功能行為的形式化模型。在上述框架中的第二部分中，我們同樣可以使用擴展形式的SysML/ MARTE狀態機模型對嵌入式系統的功能行為進行建模，作為模型轉換的源模型；并通過建立擴展狀態機元模型與時間自動機元模型之間的語義映射規則［19］，在 AMMA平臺上完成到時間 自動機目標模型的自動轉換。之后，為了能夠在時間自動機驗證工具UPPAAL上展開驗證，還通過AMMA平臺中的TCS組件將目標模型轉換成在UPPAAL工具中所接受的文本格式的模型。

最后，將上述兩個層面上轉換所得到的表示系統功能行為的時間自動機模型和表示系統安全性質的時序邏輯公式作為驗證工具UPPAAL的輸入，進行系統行為安全性質的形式化分析驗證。

4.2 SysML/MARTE狀態機與GTS的元模型轉換

為了完成上述的模型轉換與驗證框架，需要建立Sys ML/MARTE狀態機元模型與GTS的元模型之間的語義映射。但是，目前在AltaRica的相關材料中并沒有提供GTS相應的元模型，因此在本小節中我們根據AltaRica標準文檔中模型元素的說明構建了一個包含其核心建模概念的GTS元模型架構（如圖6所示）。

在此架構中，一個GTS模型包含多個節點Node（即系統組件）以及與數據相關的Domains和Constant Values等元素。其中：Domains包含Basic Domain和Compound Domain，基本域是指布爾型、整型、或者范圍、枚舉等類型，復合域則表示結構、數組等類型；Node模型元素中則包括了Transition、Event、Parameter以及Variable等。Tran-sition中包含衛式（Guard）、事件（Event）和一系列的賦值（Assignment）；Sysc用于定義Node之間的同步，Parameter用于表示在狀態前移過程中觸發可能事件所需的參數；Variables包含State Value（狀態變量）和Flow Value（流變量），其中狀態變量的值只有在事件發生時才會改變，流變量是用來表示節點輸入/輸出接口上數據通信的共享變量。結合2.2節中構造的Sys ML/MARTE狀態機的元模型及其語義信息，給出從Sys ML/MARTE狀態機元模型到GTS元模型之間的語義映射規則。以下設定S為Sys ML/MARTE狀態機的元模型，G為GTS的元模型，二者之間的語義關系Γ即定義了從S到G的映射規則集合，表示為：Γ（S）

Figure 5 Safety verification framework of the Sys ML state machine圖5 Sys ML狀態機安全性驗證框架

G，即函數Γ中包含了一系列的模型元素映射規則，如表1中所示。

映射規則Γ的定義說明包括了基本類型結構、同步以及行為等三個方面。在基本類型結構映射中，Sys ML/MARTE中支持Integer、String、Boolean、DateTime和Real，GTS的基本數據類型有Integer、String、Boolean和Range。根據語義可以直接將Integer、String、Boolean映射為Integer、String、Boolean；而Date Time映射為Integer；Real映射Integer；將Real映射為Range，其中小數點前的數表明范圍開始點，小數點后的數表明范圍結束。在同步約束映射中，Sys ML/MARTE狀態機中的Sync代表狀態機中的同步，GTS中的Sync表示各個狀態轉移的同步性，因此相互映射。在行為映射中，一個Sm映射為一個GTS；Region包含狀態 機 中 的 所有 定 義 和 元 素，映 射 到 Node；Sys ML/MARTE狀態機中的trigger觸發轉移，而GTS的Event是觸發轉移的前提，根據用途因此映射到GTS的Event；狀態機的Transition與 GTS的Transition語義是相同的，故而映射；Sys ML/MARTE狀態機中的初始狀態是Initial-Node直接映射到GTS中的初始狀態Init；Sys ML/MARTE狀態機中的guard作為轉移時必須滿足的條件，與GTS上的guard語義相同，直接映射；狀態機中的狀態（state）表明狀態機中的狀態，映射到GTS中的statevalue，因為它是作為狀態變量，表明系統中各個狀態的變化；狀態機中的action映射為GTS的flowvalue（表示系統中的數據流動）。

Table 1 Elements of structure mapping between the Sys ML/MARTE state machine and the guard transition system表1 SysML/MARTE狀態機與GTS元素映射

Figure 6 Meta-model of the GTS圖6 GTS元模型

4.3 Sys ML/MARTE狀態機與時間自動機的模型轉換

一個時間自動機A的形式化定義是一個四元組［20］，其中：N表示有窮的位置集合，I0是初始位置，E表示邊的集合，I為位置上的不變式。由于本文工作中基于時間自動機UPPAAL來進行驗證，因此在模型轉換框架中使用的時間自動機元模型是一個基于 UPPAAL的時間自動機元 模型［21］。其 元 模 型 架 構 主 要由 模板 （Template）、公共的動作集（Action）、聲明（Declare）以及時鐘集（Clock）等組合而成，每個模板都由位置（Location）、遷移（Transition）、參數（Parameter）組成。其中遷移上定義了守衛條件、源節點、目標節點；其中守衛條件包括參數表達式Parameter、表示控制的布爾表達式Expression以及標簽（Label）；Location派生出初始化的位置（Initial）以及組合標簽。

以下給出Sys ML/MARTE狀態機元模型與上述時間自動機元模型之間的語義映射規則。不妨設S是Sys ML/MARTE的元模型中的元素集合，T是時間自動機元模型中的元素集合，則二者之間的語義映射關系通過函數∮（ST來表示；即函數∮中包含了一系列的模型元素映射規則，如表2中所示。

映射規則∮的定義說明包括了基本類型結構、時間約束以及行為等三個方面。在基本類型結構映射中，Sys ML/MARTE的基本數據類型有Integer、String、Boolean、DateTime和Real等，而UPPAAL中目前支持Integer、String、Boolean數據類型，根據語義可以直接將Integer、String、Boolean映射；Date Time映射為Integer；Real取小數點前的數值映射為Integer。在時間約束映射中，Timed Instant Observation與Timed Duration Observation分別映射到時間自動機中的時鐘，通過觀察屬性的不同設置成不同的時間約束，Timed Processing表達了事件或者行為的執行時間，并包含了持續期間的屬性，使用TimeExpression描述，因此可以直接映到Boolean；Timed Event可以指定事件發生的次數（repetition屬性）或者每次發生間隔的時間（every屬性），因此直接映到Boolean。狀態機中的Region的On代表引入時鐘的模型，直接映射到時間自動機中的時鐘。在行為映射中，一個Sm映射為一個時間自動機的模板Template；Region包含狀態機的所有定義和元素，映射到時間自動機（TA）；狀態機中的Vertex同時間自動機的Location都是描述一個狀態，所以互相映射；Transition的語義同時間自動機的Transition語義是相同的，故而映射；而狀態機中的初始節點Initial Node與自動機中的初始節點Initial映射；要想發生轉移則必須滿足守衛條件，想要進入狀態必須要滿足不變式，根據constrant所在位置不同可以分別映射為guard和invariant；Sys ML狀態機中的Trigger用來觸發轉移，TA中的synchronization用于事件的同步性，因此兩者相互可以映射；Behavior表示轉移時完成的行為與時間自動機的assignment相互映射；Sys ML狀態機中的Action表明在狀態中需要完成的動作，因此與TA中的Location的賦值相互映射。

Table 2 Elements of structure mapping between the Sys ML/MARTE state machine and the timed automata表2 SysML/MARTE狀態機與時間自動機元素映射

5 基于AMMA平臺的模型轉換與安全性驗證方法實現

本小節中首先給出了前述小節所設計的模型轉換與安全性驗證框架在AMMA平臺下的具體實現方法，然后給出了一個簡要的示例說明。

5.1 基于AMMA平臺的模型轉換方法的實現

AMMA是一個在Eclipse環境下支持MDE方法的具有（元）建模、模型轉換、模型編織以及模型管理等功能的平臺［11］。本文在前面小節的工作基礎 上，在 AMMA平臺 上設 計并 實現 了 從Sys ML/MARTE狀態機模型分別到AltaRica模型以及時間自動機模型的轉換，并基于UPPAAL工具展開形式化驗證工作。具體而言，AMMA平臺中提供了一套模型轉換的核心組件：KM3（Kernel Meta Meta Model）、ATL（ATLAS Transform Language）［22，23］、TCS（Textual Concrete Syntax）［18］等。圖7是在4.1節中所設計的安全性驗證框架中基于AMMA平臺的模型轉換過程的細化。

Figure 7 Model transformation process of the AMMA platform圖7 基于AMMA平臺的模型轉換過程

基于AMMA平臺實現模型之間的語義映射過程實質上是通過ATL語言定義ATL轉換規則的過程。我們通過ATL中的命令式指令來聲明源模型（Sys ML/MARTE狀態機模型）和目標模型（GTS模型）之間的元素關系，然后通過ATL虛擬機的執行將源模型轉換為目標模型。在 AMMA平臺中我們定義的Sys ML/MARTE狀態機元模型與GTS元模型如圖8和圖9所示，其中包括了構建Sys ML/MARTE活動圖元模型與GTS元模型中的每個類，定義每個類中的屬性以及類與類之間的關系等。MMs和MMt是Sys ML/ MARTE狀態機元模型和GTS元模型。Model-Transform.alt是針對Sys ML/MARTE狀態機元模型與GTS元模型在Eclipse的ATL工程下定義的轉換文件，通過 ATL虛擬機對轉換規則的執行，就可以將Sys ML/MARTE狀態機源模型轉換成GTS目標模型。表3是在ATL工程中用XMI格式描述的GTS元模型示例。

Figure 8 Meta-model of SysML/MARTE state machine based-on ATL圖8 基于ATL的Sys ML/MARTE狀態機元模型

Figure 9 Meta-model of the GTS diagram based-on the ATL圖9 基于ATL的GTS元模型

Table 3 Description of the Guard_Transition class based-on the XMI表3 基于XMI的Guard_Transition類描述

5.2 實例說明

以下給出了一個飛機著陸控制系統的簡單實例說明。飛機著陸控制系統實例的詳細說明可參見文獻［20，24］，主要包括兩組控制對象：飛機（aircraft）和跑道（runway），其中每架飛機具有預計到達時間、最早/最晚到達時間、飛行速度、燃油消耗、是否延誤等屬性，跑道具有占用時間、進近飛機號、等待飛機號、間隔時間等屬性。圖10中分別給出了飛機著陸控制系統部分的Sys ML/ MARTE狀態機模型（建模工具采用的是Raphsody［25］）。在 狀 態 機 模 型 中 主要引 用 了 兩 個MARTE建模元素，分別為時鐘元素Clock以及資源使用元素Resource Usage，具體名字是時間time和燃油消耗energy，time是飛機到達時間的時鐘變量，而energy是飛機消耗的燃油量。

圖11表示在5.1節所建立的模型轉換框架的主要ATL配置信息過程中，分別設定Sys ML/ MARTE狀態機元模型和GTS元模型的文件，并定義輸出到目標GTS模型文件中。當我們得到目標GTS模型后，則可以繼續通過AltaRica工具［26］（如圖12所示）獲得系統故障樹模型以及表示系統安全性質的時序邏輯公式，所得到安全性質公式示例如下：

Figure 11 ATL configuration圖11 ATL配置

（1）E＜＞KL101.done and KL108.done andKL136.done and KL143.done

Figure 12 Interface of the Altarica Studio圖12 AltaRica Studio界面

語義描述：著陸系統最終應該將所有空中的飛機都成功地引導落地，不可以出現永遠有飛機在空中。

（2）A［］runway0.Idle And In Use imply runway0.Idle AndIn Use

語義描述：處在Idle And In Use的runway0一定還會進入Idle AndInUse狀態，即跑道不能永遠被占用。

（3）E＜＞KL101.delayed and KL108.on_ time

Figure 10 Aircraft's Sys ML state machine diagram圖10 飛機著陸系統的部分狀態機模型

描述：表示飛機KL101和飛機KL108可以同時處在delayed狀態和approaching狀態。

此外，從Sys ML/MARTE建模得到的飛機著陸狀態圖經過ATL模型轉換以及TCS文本轉換可以得到相應的時間自動機驗證模型，并將轉換結果導入到UPPAAL中。圖13給出了導入到UPPAAL中的著陸系統的時間自動機模型（在本例中設置飛機的數量為4個，跑道數量為2個）。

飛機著落控制系統的安全性示例驗證如下（如圖14所示）：

（1）E＜＞KL101.done and KL108.done and KL136.done and KL143.done//驗證結果：滿足

（2）A［］runway0.Idle AndIn Use imply runway0.Idle AndIn Use//驗證結果：滿足

（3）E＜＞KL101.delayed and KL108.on_ time//驗證結果：滿足

6 結束語

與本文相關的研究工作可以分為如下三個方面：第一類工作表明了UML/Sys ML與MARTE的結合使用能夠有效地對復雜嵌入式系統的設計進行建模分析，如：文獻［24］研究了將UML圖（狀態機、時序圖、活動圖）結合 MARTE轉換成價格時間自動機并進行驗證的方法；文獻［27］設計了將UML/MARTE模型向FIACRE形式模型的轉換框架，這些轉換也是建立在 AMMA平臺上利用ATL和TCS來完成；文獻［28］研究了基于MDE的實時系統UML模型到形式化模型的模型轉換，并進一步進行系統安全性質的形式化證明；文獻［19］則給出了Sys ML狀態機到時間自動機的轉換過程等。第二類工作是與安全性建模與分析語言AltaRica相關的，如：文獻［14］中介紹了AltaRica模型，以及在形式化驗證中可以發揮的作用；文獻［9］研究了如何利用形式化工具來進行AltaRica模型的驗證，設計了從AltaRica模型轉換到NuSMV的模型轉換方法；文獻［16］則詳細給出了將AltaRica的語義模型GTS轉換成故障樹的算法；文獻［10］給出了AltaRica及其相關工具在航空系統實例中的應用及分析等。第三類相關研究工作是模型驅動工程與形式化方法相結合；如：文獻［29］討論了形式化驗證工具可以用在基于模型的開發過程中用來降低降低成本、提高系統開發質量；文獻［30］研究了將Sys ML和形式化模型進行

Figure 13 Timed automata model of aitcraft landing in the UPPAAL圖13 UPPAAL中飛機著落系統的時間自動機模型

Figure 14 Results of verification圖14 驗證結果

結合并進行系統安全性分析驗證的方法；文獻［31］提出了將Sys ML時序圖轉換成時間自動機并進行形式化驗證的方法等。

相比較而言，本文工作是提出了一種基于模型驅動架構的面向Sys ML/MARTE狀態機的系統安全性驗證方法，具體包括：構建了具備Sys ML/ MARTE擴展語義的狀態機元模型，以及安全性建模與分析語言AltaRica的語義模型GTS的元模型；然后建立了從Sys ML/MARTE狀態機模型分別到時間自動機模型以及AltaRica模型的語義映射模型轉換規則；并基于AMMA平臺和時間自動機驗證工具UPPAAL設計實現了對Sys ML/ MARTE狀態機的模型轉換與系統安全性形式化驗證的框架，實現了基于模型驅動的嵌入式系統設計安全性驗證的一種方法。在接下來進一步的工作中，我們將對具有并發結構的狀態機模型的語義轉換展開研究，并結合實際工程中某機載航電系統的安全性分析需求展開本文方法的實際應用驗證。此外，本文主要研究的是利用現有的一些工具系統，并從技術層面提出了方法和框架進行安全性方法研究，沒有從理論層面特別是形式化角度證明模型間語法和語義轉換的正確性和完全性問題，這是我接下來進行研究的工作之一。

［1］ Roudier Y，Idrees M S，Apvrille L.Towards the model-driven engineering of safety requirements for embedded systems ［C］∥Proc of IEEE 2013 International Workshop on Model-Driven Requirements Engineering（MoDRE），2013：55-64.

［2］ Hutchinson J，Rouncefield M，Whittle J.Model-driven engineering practices in industry［C］∥Proc of IEEE the 33rd International Conference on Software Engineering（ICSE），2011：633-642.

［3］ H?stbacka D，Veps?l?inen T，Kuikka S.Model-driven development of industrial process control applications［J］.Journal of Systems and Software，2011，84（7）：1100-1113.

［4］ Moy Y，Ledinot E，Delseny H，et al.Testing or formal verification：DO-178C alternatives and industrial experience［J］. IEEE Software，2013，30（3）：50-57.

［5］ Reif W.Model based safety analysis［C］∥Proc of Dependable Control of Discrete Systems，2009：3.

［6］ Biehl M，Dejiu C，T?rngren M.Integrating safety analysis into the model-based development toolchain of automotive embedded systems［C］∥Proc of ACM Sigplan Notices，2010：125-132.

［7］ Friedenthal S，Moore A，Steiner R.A practical guide to SysML：The systems modeling language［M］.New York： Elsevier，2011.

［8］ Selic B，Gérard S.Modeling and analysis of real-time and embedded systems with UML and MARTE：Developing cyber-physical systems［M］.New York：Elsevier，2013.

［9］ Bozzano M，Cimatti A，Lisagor O，et al.Symbolic model checking and safety assessment of altarica models［J］.Electronic Communications of the EASST，2011，46（2011）：1.

［10］ Bieber P，Bougnol C，Castel C，et al.Safety assessment with AltaRica-lessons learnt based on two aircraft system studies［C］∥Proc of the 18th IFIP World Computer Congress，Topical Day on New Methods for Avionics Certification.Citeseer，2004：1.

［11］ Atlan Mod Team，INRIA.AMMA home［EB/OL］.［2008-01-07］.http：//wiki.eclipse.org/index.php/AMMA.

［12］ Rioux L，Saunier T，Gérard S，et al.MARTE：A new profile RFP for the modeling and analysis of real-time embedded systems［C］∥Proc of UML-SoC'05，2005：1.

［13］ Güdemann M.Qualitative and quantitative formal modelbased safety analysis［D］.Magdeburg：Ottovon Guericke U-niversity，2011.

［14］ Prosvirnova T，Batteux M，Brameret P，et al.The altarica 3.0 project for model-based safety assessment［C］∥Proc of IEEE the 4th IFAC Workshop on Dependable Control of Discrete Systems（DCDS），2013：1.

［15］ Rauzy A B.Guarded transition systems：A new states/events formalism for reliability studies［J］.Proceedings of the Institution of Mechanical Engineers，Part O：Journal of Risk and Reliability，2008，222（4）：495-505.

［16］ Prosvirnova T，Rauzy A.AltaRica 3.0 project：Compile guarded transition systems into fault trees［J］.Proceedings of ESREL2013，2013，20（3）：485-491.

［17］ Rutle A，Rossini A，Lamo Y，et al.A formal approach to the specification and transformation of constraints in MDE ［J］.The Journal of Logic and Algebraic Programming，2012，81（4）：422-457.

［18］ Ruscio D D，Iovino L，Pierantonio A.Managing the coupled evolution of metamodels and textual concrete Syntax specifications［C］∥Proc of IEEE the 39th EUROMICRO Conference on Software Engineering and Advanced Applications（SEAA），2013：114-121.

［19］ Huang Xiao-pu.Research on MDE based model transformation［D］.Nanjing：Nanjing University，2013.（in Chinese）

［20］ Behrmann G，David A，Larsen K G，et al.UPPAAL 4.0 ［C］∥Proc of IEEE the 3 rd International Conference on Quantitative Evaluation of Systems（QEST 2006），2006：125-126.

［21］ UPPAAL tutorial［EB/OL］.［2013-01-09］.http：//w ww. it.uu.se/research/group/darts/uppaal/flat-1_1.dtd.

［22］ Jouault F，Tisi M.Towards incremental execution of ATL transformations［M］∥Theory and Practice of Model Transformations，Berlin：Springer，2010：123-137.

［23］ ATLAS group，LINA&INRIA Nantes.ATL：Atlas trans-for-Mationlanguage［EB/OL］.［2006-01-01］.http//www.eclipse.org/m2m/atl/doc/ATL_User_Manual%5Bv07%5D. pdf，2006.

［24］ Ji Ming.The method research on resource modeling and verification of real-time software based on model transformation［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2010.（in Chinese）

［25］ Harel D，Kugler H.The rhapsody semantics of statecharts （or，on the executable core of the U ML）［M］∥Integration of Software Specification Techniques for Applications in Engineering，Berlin：Springer，2004：325-354.

［26］ Rauzy A.AltaRica Down Load［EB/OL］.［2014-12-07］.http//www.eclipse.org/m2m/atl/http：//altarica.labri.fr/ pub/tools/packages/current/arc-current.tar.gz.

［27］ Zhang Tian，Jouault F，Attiogbe C.MDE-Based model to FIACRE model［J］.Journal of Software，2009，20（2）：214-233.（in Chinese）

［28］ Liu Ya-ping，Research on model transformation method of real-time system based on metamodeling［D］.Nanjing：Nanjing University of Aeronautics and Astronautics，2010.（in Chinese）

［29］ Whalen M，Cofer D，Miller S，et al.Integration of formal analysis into a model-based software development process ［M］∥Formal Methods for Industrial Critical Systems，Berlin：Springer，2008：68-84.

［30］ Pétin J，Evrot D，Morel G，et al.Combining Sys ML and formal methods for safety requirements verification［C］∥Proc of the 22nd International Conference on Software& Systems Engineering and their Applications，2010：115-122.

［31］ Cui Kang-le.Research on UML timing diagram model to UPPAAL timed automata model transformation method and its tool to achieve［D］.Shanghai：East China Normal University，2011.（in Chinese）

附中文參考文獻：

［19］ 黃小浦.基于 MDE模型轉換的若干研究［D］.南京：南京大學，2013.

［24］ 吉鳴.基于模型轉換的實時軟件資源建模與驗證的方法研究［D］.南京：南京航空航天大學，2010.

［27］ 張天，Jouault F，Attiogbe C，等.基于MDE的異構模型轉換從MARTE模型到FIACRE模型［J］.軟件學報，2009，20 （2）：214-233.

［28］ 劉亞萍.基于MDE的UML模型到形式化模型的轉換方法研究［D］.南京：南京航空航天大學，2009.

［31］ 崔康樂.UML時序圖模型到UPPAAL時間自動機模型轉換方法研究和工具實現［D］.上海：華東師范大學，2011.

劉雪（1989），女，安徽宿州人，碩士生，研究方向為軟件工程和軟件建模與分析。E-mail：lx_029@nuaa.edu.cn

LIU Xue，born in 1989，MS candidate，her research interests include software engineering，and software modeling and analysis.

胡軍（1973），男，湖北黃岡人，博士，副教授，研究方向為模型驅動的系統安全性分析、軟件驗證和嵌入式系統設計。E-mail：hujun.nju@139.com

HU Jun，born in 1973，PhD，associate professor，his research interests include model-based safety analysis，software analysis，and formal methods.

黃志球（1965 ），男，江蘇南京人，博士后，博士生導師，研究方向為軟件工程和軟件度量。E-mail：zqhuang@nuaa.edu.cn

HUANG Zhi-qiu，born in 1965，post doctor，PhD supervisor，his research interests include software engineering，and software metrics.

馬金晶（1990 ），男，安徽合肥人，碩士生，研究方向為軟件分析和模型檢測。E-mail：majinjing3@vip.qq.com

MA Jin-Jing，born in 1990，MS candidate，his research interests include software analysis，and model checking.

程楨（1990 ），男，安徽安慶人，碩士生，研究方向為軟件分析和模型檢測。E-mail：604246353@qq.com

CHENG Zhen，born in 1990，MS candidate，his research interests include software analysis，and model checking.

石嬌潔（1990 ），女，河南鄭州人，碩士生，研究方向為軟件分析和模型檢測。E-mail：shijiaojiexzs@163.com

SHI Jiao-jie，born in 1990，MS candidate，her research interests include software analysis，and model checking.

Research on model driven safety verification for embedded system designs

LIU Xue1，HU Jun1，2，HUANG Zhi-qiu1，MA Jin-jing1，CHENG Zhen1，SHI Jiao-jie1
（1.School of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing 210016；
2.State Key Laboratory for Novel Software Technology，Nanjing University，Nanjing 210093，China）

In recent years the model based safety analysis and verification method for embedded systems is an important research hotspot in the field of safety critical systems engineering.We put forward a system safety verification method based on the model driven architecture，which is Sys ML/MARTE state machine oriented，including the construction of both the state machine metamodel which has Sys ML/MARTE extension semantics，and the GTS metamodel which is the semantic model of AltaRica （ie.safety modeling and analysis language）.We then establish semantic mapping model transformation rules from a Sys ML/MARTE state machine model to the timed automata model and to the AltaRica model respectively.Thirdly，based on the platform of the AMMA and the timed automata verification tools UPPAAL we design and realize the model transformation of the Sys ML/MARTE state machine and the framework for system safety formal verification.Finally a safety verification example about aircraft landing control system design model is analyzed.

system safety analysis；model-driven engineering；Sys ML/MARTE；state machine model；embedded system

TP311.5

A

10.3969/j.issn.1007-130X.2015.08.013

1007-130X（2015）08-1498-12

2014-09-01；

2014-11-25

國家重點基礎研究發展計劃973計劃資助項目（2014CB744904）；國家自然科學基金資助項目（61100034，61170043）；南

京航空航天大學青年科技創新基金資助項目（NS2014098）；回國留學人員科研啟動基金資助項目（2012）

通信地址：210016江蘇省南京市南京航空航天大學計算機科學與技術學院

Address：School of Computer Science and Technology，Nanjing University of Aeronautics and Astronautics，Nanjing 210016，Jiangsu，

P.R.China