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

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

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

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

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

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