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

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

2.南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室，江蘇 南京 210093）

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

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

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

2.南京大學(xué)計(jì)算機(jī)軟件新技術(shù)國家重點(diǎn)實(shí)驗(yàn)室，江蘇 南京 210093）

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

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

1 引言

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

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

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

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

2 Sys ML/MARTE模型

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

2.1 Sys ML與MARTE概述

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

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

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

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

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

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

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

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

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

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

3 AltaRica模型

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

在此架構(gòu)中，一個(gè)GTS模型包含多個(gè)節(jié)點(diǎn)Node（即系統(tǒng)組件）以及與數(shù)據(jù)相關(guān)的Domains和Constant Values等元素。其中：Domains包含Basic Domain和Compound Domain，基本域是指布爾型、整型、或者范圍、枚舉等類型，復(fù)合域則表示結(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ā)生時(shí)才會(huì)改變，流變量是用來表示節(jié)點(diǎn)輸入/輸出接口上數(shù)據(jù)通信的共享變量。結(jié)合2.2節(jié)中構(gòu)造的Sys ML/MARTE狀態(tài)機(jī)的元模型及其語義信息，給出從Sys ML/MARTE狀態(tài)機(jī)元模型到GTS元模型之間的語義映射規(guī)則。以下設(shè)定S為Sys ML/MARTE狀態(tài)機(jī)的元模型，G為GTS的元模型，二者之間的語義關(guān)系Γ即定義了從S到G的映射規(guī)則集合，表示為：Γ（S）

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

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

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

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

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

4.3 Sys ML/MARTE狀態(tài)機(jī)與時(shí)間自動(dòng)機(jī)的模型轉(zhuǎn)換

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

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

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

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

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

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

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

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

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

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

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

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 實(shí)例說明

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

圖11表示在5.1節(jié)所建立的模型轉(zhuǎn)換框架的主要ATL配置信息過程中，分別設(shè)定Sys ML/ MARTE狀態(tài)機(jī)元模型和GTS元模型的文件，并定義輸出到目標(biāo)GTS模型文件中。當(dāng)我們得到目標(biāo)GTS模型后，則可以繼續(xù)通過AltaRica工具［26］（如圖12所示）獲得系統(tǒng)故障樹模型以及表示系統(tǒng)安全性質(zhì)的時(shí)序邏輯公式，所得到安全性質(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)最終應(yīng)該將所有空中的飛機(jī)都成功地引導(dǎo)落地，不可以出現(xiàn)永遠(yuǎn)有飛機(jī)在空中。

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

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

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

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

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

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

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

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

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

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

6 結(jié)束語

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

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

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

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

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

附中文參考文獻(xiàn)：

［19］ 黃小浦.基于 MDE模型轉(zhuǎn)換的若干研究［D］.南京：南京大學(xué)，2013.

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

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

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

［31］ 崔康樂.UML時(shí)序圖模型到UPPAAL時(shí)間自動(dòng)機(jī)模型轉(zhuǎn)換方法研究和工具實(shí)現(xiàn)［D］.上海：華東師范大學(xué)，2011.

劉雪（1989），女，安徽宿州人，碩士生，研究方向?yàn)檐浖こ毯蛙浖Ｅc分析。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），男，湖北黃岡人，博士，副教授，研究方向?yàn)槟Ｐ万?qū)動(dòng)的系統(tǒng)安全性分析、軟件驗(yàn)證和嵌入式系統(tǒng)設(shè)計(jì)。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 ），男，江蘇南京人，博士后，博士生導(dǎo)師，研究方向?yàn)檐浖こ毯蛙浖攘?。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 ），男，安徽合肥人，碩士生，研究方向?yàn)檐浖治龊湍Ｐ蜋z測(cè)。E-mail：majinjing3@vip.qq.com

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

程楨（1990 ），男，安徽安慶人，碩士生，研究方向?yàn)檐浖治龊湍Ｐ蜋z測(cè)。E-mail：604246353@qq.com

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

石嬌潔（1990 ），女，河南鄭州人，碩士生，研究方向?yàn)檐浖治龊湍Ｐ蜋z測(cè)。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

國家重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃973計(jì)劃資助項(xiàng)目（2014CB744904）；國家自然科學(xué)基金資助項(xiàng)目（61100034，61170043）；南

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

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

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

P.R.China