基于SysML活動(dòng)圖的嵌入式實(shí)時(shí)系統(tǒng)安全性驗(yàn)證方法研究.pdf

1、嵌入式實(shí)時(shí)系統(tǒng)在航空航天、核電及交通等安全關(guān)鍵領(lǐng)域中廣泛使用，規(guī)模變得愈發(fā)龐大，體系結(jié)構(gòu)變得更復(fù)雜，其故障引起的安全事故有著顯著的社會(huì)影響，甚至造成災(zāi)難性的后果。因此，對(duì)嵌入式實(shí)時(shí)系統(tǒng)設(shè)計(jì)進(jìn)行安全性分析與驗(yàn)證成為學(xué)術(shù)界和工業(yè)界亟需攻克的難點(diǎn)。UML(United Modeling Language)常被用來軟件設(shè)計(jì)建模，但在建模能力上不能滿足嵌入式實(shí)時(shí)系統(tǒng)建模需求且缺乏非功能屬性建模元素；半形式化的模型在安全性驗(yàn)證上難以被直接使用。

2、r>　　針對(duì)以上問題，本文提出一種擴(kuò)展MARTE(Modeling and Analysis of Real-time and Embedded Systems)時(shí)鐘語(yǔ)義信息到SysML(System Modeling Language)活動(dòng)圖(SysML/MARTE活動(dòng)圖)的嵌入式實(shí)時(shí)系統(tǒng)安全性驗(yàn)證方法，彌補(bǔ)了UML在針對(duì)嵌入式實(shí)時(shí)系統(tǒng)建模及驗(yàn)證上的不足。主要內(nèi)容如下：
　　首先，針對(duì)嵌入式實(shí)時(shí)系統(tǒng)，提出使用SysML/MART

3、E活動(dòng)圖對(duì)嵌入式實(shí)時(shí)系統(tǒng)進(jìn)行建模，包括采用適合系統(tǒng)建模的SysML活動(dòng)圖構(gòu)建功能流模型及擴(kuò)展MARTE時(shí)鐘語(yǔ)義來構(gòu)建時(shí)間非功能屬性。然后，通過基于元模型的模型轉(zhuǎn)換方法將SysML/MARTE活動(dòng)圖轉(zhuǎn)換到時(shí)間自動(dòng)機(jī)，包括：(1)針對(duì)SysML活動(dòng)圖以及 MARTE時(shí)鐘等建模元素，分別構(gòu)建其同構(gòu)的元模型，并在元模型體系中將 MARTE語(yǔ)義信息添加到 SysML活動(dòng)圖，構(gòu)建時(shí)間自動(dòng)機(jī)的元模型；(2)給出SysML/MARTE活動(dòng)圖和時(shí)間自動(dòng)機(jī)

4、的元模型在類型、行為以及時(shí)間等元素上的語(yǔ)義映射規(guī)則，給出SysML/MARTE活動(dòng)圖嵌套、分支和并發(fā)結(jié)構(gòu)到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換規(guī)則，將SysML/MARTE活動(dòng)圖模型轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)模型；(3)通過語(yǔ)法轉(zhuǎn)換，將時(shí)間自動(dòng)機(jī)模型轉(zhuǎn)換為模型檢測(cè)工具UPPAAL可以直接使用的時(shí)間自動(dòng)機(jī)文本。最后，根據(jù)嵌入式實(shí)時(shí)系統(tǒng)設(shè)計(jì)安全需求，提取CTL(computation temporal logic)規(guī)約，在UPPAAL下對(duì)轉(zhuǎn)換得到的時(shí)間自動(dòng)機(jī)進(jìn)行安全性分