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

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

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

模型驅(qū)動的嵌入式系統(tǒng)設(shè)計安全性驗證方法研究*

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

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

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

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

系統(tǒng)安全性分析；模型驅(qū)動工程；Sys ML/MARTE；狀態(tài)機模型；嵌入式系統(tǒng)

1 引言

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

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

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

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

2 Sys ML/MARTE模型

本節(jié)主要介紹系統(tǒng)建模語言 Sys ML和MARTE模型，并針對Sys ML中的狀態(tài)機模型，給出了在本文工作中所構(gòu)造的結(jié)合MARTE語義信息的擴展狀態(tài)機的元模型，為后面工作提供模型轉(zhuǎn)換與驗證的基礎(chǔ)。

2.1 Sys ML與MARTE概述

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

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

Figure 1 Package structure of the MARTE圖1 MARTE建模元素包的總體結(jié)構(gòu)圖

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

2.2 SysML/MARTE的狀態(tài)機及其元模型構(gòu)造

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

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

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

Figure 2 Sys ML state machine diagram of the counting function圖2 計數(shù)功能的Sys ML狀態(tài)機示例

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

3 AltaRica模型

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

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

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

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

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

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

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

4 系統(tǒng)安全性驗證框架

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

4.1 基于模型轉(zhuǎn)換的安全性驗證框架

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

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

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

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

4.2 SysML/MARTE狀態(tài)機與GTS的元模型轉(zhuǎn)換

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

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

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

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

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

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

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

4.3 Sys ML/MARTE狀態(tài)機與時間自動機的模型轉(zhuǎn)換

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

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

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

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

5 基于AMMA平臺的模型轉(zhuǎn)換與安全性驗證方法實現(xiàn)

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

5.1 基于AMMA平臺的模型轉(zhuǎn)換方法的實現(xiàn)

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

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

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

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

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 實例說明

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

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

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界面

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

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

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

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

Figure 10 Aircraft's Sys ML state machine diagram圖10 飛機著陸系統(tǒng)的部分狀態(tài)機模型

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

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

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

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

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

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

6 結(jié)束語

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

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

Figure 14 Results of verification圖14 驗證結(jié)果

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

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

［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模型轉(zhuǎn)換的若干研究［D］.南京：南京大學，2013.

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

［27］ 張?zhí)?，Jouault F，Attiogbe C，等.基于MDE的異構(gòu)模型轉(zhuǎn)換從MARTE模型到FIACRE模型［J］.軟件學報，2009，20 （2）：214-233.

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

［31］ 崔康樂.UML時序圖模型到UPPAAL時間自動機模型轉(zhuǎn)換方法研究和工具實現(xiàn)［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），男，湖北黃岡人，博士，副教授，研究方向為模型驅(qū)動的系統(tǒng)安全性分析、軟件驗證和嵌入式系統(tǒng)設(shè)計。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

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

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

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

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

P.R.China