1、近年來在安全關(guān)鍵應(yīng)用領(lǐng)域中（如：航空、交通、核電站等）嵌入式系統(tǒng)及軟件的規(guī)模增大以及系統(tǒng)復(fù)雜度的迅速增加帶來了嵌入式系統(tǒng)及軟件安全性保障方面的重要挑戰(zhàn)；與此同時，模型驅(qū)動的系統(tǒng)／軟件開發(fā)技術(shù)在安全關(guān)鍵工程領(lǐng)域中也開始得到廣泛的關(guān)注和應(yīng)用。傳統(tǒng)的統(tǒng)一建模語言（如：UML，SysML等）已經(jīng)越來越多的應(yīng)用于系統(tǒng)及軟件建模，但在面向安全關(guān)鍵領(lǐng)域時這些建模語言及方法目前還存在一些問題，如：本身缺乏對實時嵌入式系統(tǒng)的非功能行為描述的元素及機制（包

2、括：對時間、資源、概率的有效建模等）；建模語言尚缺少模型語義的精確定義，這對使用軟件模型展開面向安全性的形式化驗證與分析時帶來困難等等。
　　本文工作主要是對模型驅(qū)動架構(gòu)（MDA）下的嵌入式系統(tǒng)模型的安全性分析問題展開了研究，探索了基于模型轉(zhuǎn)換的SysML/MARTE狀態(tài)機、AltaRica模型以及時間自動機的UPPAAL模型的安全性分析與驗證方法，具體包括以下幾個部分：
　　(1)研究了基于SysML/MARTE的復(fù)雜嵌入

3、式系統(tǒng)設(shè)計建模問題；系統(tǒng)建模語言 SysML是目前系統(tǒng)工程應(yīng)用開發(fā)的標(biāo)準(zhǔn)建模語言，MARTE主要從時間約束、資源分配等非功能屬性方面來對嵌入式系統(tǒng)建模與分析。本文以 SysML狀態(tài)機模型作為一個典型的研究對象，結(jié)合MARTE中包括時間、概率等信息在內(nèi)的非功能資源方面的語義擴展，用以對復(fù)雜嵌入式系統(tǒng)的行為進行建模。
　　(2)對MDA的一個核心問題：模型轉(zhuǎn)換展開了基于AMMA平臺的異構(gòu)模型間轉(zhuǎn)換的方法，包括：建立SysML/MART

4、E狀態(tài)機元模型、AltaRica元模型和時間自動機元模型，以及模型之間的語義映射關(guān)系，然后基于AMMA平臺的模型轉(zhuǎn)換語言ATL構(gòu)造模型轉(zhuǎn)換規(guī)則，為在模型驅(qū)動架構(gòu)下實現(xiàn)從SysML/MARTE狀態(tài)機模型分別到AltaRica模型、時間自動機模型的轉(zhuǎn)換建立了基礎(chǔ)。
　　(3)研究了SysML/MARTE狀態(tài)機模型在時間屬性方面的安全性分析與驗證方法；通過元模型的語義映射關(guān)系，將SysML/MARTE狀態(tài)機模型轉(zhuǎn)換到時間自動機模型，所需

5、要滿足的時序邏輯公式從AltaRica模型中獲取，然后采用分析工具UPPAAL進行安全性的分析與驗證。
　　(4)研究了從系統(tǒng)概率屬性方面面向 SysML/MARTE狀態(tài)機模型的安全性驗證問題；包括：將SysML/MARTE狀態(tài)機模型轉(zhuǎn)換到AltaRica模型，生成故障樹模型，并將得到的故障樹作為故障樹分析工具XFTA的輸入，進而展開對系統(tǒng)安全分析性和驗證。
　　(5)設(shè)計了一個基于模型的對嵌入式系統(tǒng)設(shè)計分析的框架，并分別通