- 相關(guān)推薦
淺析基于BIP 的AADL 行為模型驗(yàn)證方法的論文
1 前言
隨著嵌入式系統(tǒng)越來越多的應(yīng)用在工業(yè)控制、車載電子、航天航空電子等任務(wù)關(guān)鍵和實(shí)時(shí)系統(tǒng)，它的復(fù)雜度和性能要求也越來越高。傳統(tǒng)的以代碼為核心的開發(fā)方法逐步從代碼為中心的開發(fā)提前到以模型驅(qū)動(dòng)開發(fā)為核心。以供在早期對系統(tǒng)進(jìn)行設(shè)計(jì)驗(yàn)證，減少不必要的損失。為此，美國汽車工程師協(xié)會(huì)在2004 年提出了體系結(jié)構(gòu)建模語言AADL(architecturalanalysis and design language, AADL)，并發(fā)布為SAE AS5506 標(biāo)準(zhǔn)，目的是提供一種標(biāo)準(zhǔn)而又足夠精確的方式，設(shè)計(jì)與分析嵌入式實(shí)時(shí)系統(tǒng)的軟、硬件體系結(jié)構(gòu)及功能和非功能性質(zhì)。由于AADL 具有語法簡單、功能強(qiáng)大、可擴(kuò)展等優(yōu)點(diǎn)，他已經(jīng)逐步成為工業(yè)界事實(shí)上的標(biāo)準(zhǔn)。根據(jù)現(xiàn)有的形式化驗(yàn)證工具的應(yīng)用情況，本文通過制定映射規(guī)則，將AADL 行為模型直接轉(zhuǎn)換成BIP 模型。并且利用已有的BIP 模型工具對準(zhǔn)換后的BIP 模型進(jìn)行驗(yàn)證。提供一種形式化的驗(yàn)證AADL 行為模型的新途徑，如圖1 所示。
2 BIP構(gòu)件模型
BIP(Behavior,Interaction,Priority) 是Verimag 提出的實(shí)時(shí)系統(tǒng)建模語言，采用自動(dòng)機(jī)的方式描述行為，并且支持異構(gòu)構(gòu)件之間的組合。BIP 模型工具能夠用來分析模型和可執(zhí)行代碼。BIP 語言對系統(tǒng)的形式化描述主要由下面三部分組成：
原子構(gòu)件：即帶有行為描述的構(gòu)件，這些行為包含了遷移，空交互和優(yōu)先級。觸發(fā)的遷移包括端口，這些端口帶有動(dòng)作名稱，可用于端口同步。
連接件：用于描述原子構(gòu)件端口之間可能的交互模式。
優(yōu)先級關(guān)系：用于在幾種可能的交互方式中做選擇，這種選擇需要根據(jù)條件來判斷。條件和原子構(gòu)件整體的狀態(tài)有關(guān)。下面詳細(xì)闡述這個(gè)語言的主要特征。
2.1 優(yōu)先權(quán)
在包含多個(gè)構(gòu)件交互的系統(tǒng)里，優(yōu)先權(quán)可以根據(jù)條件來確定所有執(zhí)行交互的優(yōu)先級。因此優(yōu)先權(quán)可以通過設(shè)置執(zhí)行遷移約束條件來減少系統(tǒng)的非確定性。這些條件是一套規(guī)則，每條規(guī)則都由和條件交互有關(guān)的命令對組成。條件是一個(gè)與構(gòu)件交互變量有關(guān)的布爾表達(dá)式。當(dāng)條件滿足，所有交互都可執(zhí)行，則優(yōu)先級高的先執(zhí)行。對于靜態(tài)優(yōu)先級，條件可以忽略。規(guī)則也可以擴(kuò)展為交互組合。例如規(guī)則P1< 的優(yōu)先權(quán)高于p 有著比p1|q更高的優(yōu)先權(quán)。此外，優(yōu)先權(quán)和交互是兼容的，p|q>
3 AADL行為模型到BIP模型的轉(zhuǎn)換規(guī)則
AADL 模型轉(zhuǎn)換主要是建立AADL 模型與目標(biāo)模型元素的轉(zhuǎn)換規(guī)則。本文從AADL模型的行為模型出發(fā)，建立其到BIP 模型的轉(zhuǎn)換規(guī)則。AADL 行為模型用于描述構(gòu)件內(nèi)部的詳細(xì)行為模式，與其他構(gòu)件通過端口連接等方式形成的流(包括數(shù)據(jù)流和時(shí)間流)進(jìn)行交互。AADL 模型中每個(gè)構(gòu)件內(nèi)的行為模型相對對立，可以直接映射成BIP 描述的原子構(gòu)件，多個(gè)構(gòu)件交互的行為可以映射為BIP 復(fù)合構(gòu)件里多個(gè)原子構(gòu)件的交互，從而避免了構(gòu)造自動(dòng)機(jī)的積的復(fù)雜過程。
4 關(guān)鍵系統(tǒng)的任務(wù)轉(zhuǎn)換實(shí)例
對于實(shí)時(shí)的關(guān)鍵系統(tǒng)，系統(tǒng)里具有更高優(yōu)先級的任務(wù)必須能夠搶占正在執(zhí)行的任務(wù)，并且在任務(wù)執(zhí)行完成后恢復(fù)被搶占任務(wù)的執(zhí)行。這既是系統(tǒng)的實(shí)時(shí)要求，又是系統(tǒng)的安全性要求。對于以汽車電子，航空電子，航空控制系統(tǒng)等為代表的實(shí)施關(guān)鍵系統(tǒng)，必須建立能夠描述任務(wù)執(zhí)行的所有可能狀態(tài)，正確的描述系統(tǒng)任務(wù)狀態(tài)的遷移過程，對系統(tǒng)執(zhí)行進(jìn)行分析。
4.1 關(guān)鍵系統(tǒng)任務(wù)的AADL行為描述
本文首先用AADL 行為模型附件語法來為一個(gè)可搶占實(shí)時(shí)任務(wù)進(jìn)行建模，然后將這個(gè)實(shí)時(shí)模型的可搶占執(zhí)行模型轉(zhuǎn)換成BIP 行為模型的狀態(tài)遷移過程，并對BIP 模型進(jìn)行驗(yàn)證。因?yàn)檫w移的條件比較復(fù)發(fā)，對于研究實(shí)時(shí)任務(wù)的搶占執(zhí)行不具有普遍一起，所以本文簡化的描述了AADL 狀態(tài)的可搶占執(zhí)行到BIP 模型的轉(zhuǎn)換過程。
4.2 BIP模型驗(yàn)證
對于轉(zhuǎn)換而成的BIP 模型，我們可以用驗(yàn)證工具Aldebaran 進(jìn)行死鎖檢測。這個(gè)工具主要是對BIP 模型的結(jié)構(gòu)進(jìn)行分析，它的原理是首先它使用前端引擎來探索BIP 模型的所有運(yùn)行狀態(tài)，并將這些狀態(tài)轉(zhuǎn)換成一個(gè)帶標(biāo)記的遷移系統(tǒng)，然后將這個(gè)帶標(biāo)記的遷移系統(tǒng)作為作為檢測工具的后端輸入，然后對系統(tǒng)進(jìn)行死鎖檢測。
如果對于具有并發(fā)執(zhí)行或者對執(zhí)行時(shí)間嚴(yán)格的狀態(tài)轉(zhuǎn)換，我們可以通過設(shè)置狀態(tài)轉(zhuǎn)化的優(yōu)先級或者在模型端口里加入時(shí)間變量。通過其他的BIP 模型檢測器來驗(yàn)證。文獻(xiàn)舉例驗(yàn)證了構(gòu)件之間通過端口的同步交互，這種方法可以擴(kuò)展到對AADL 行為模型的狀態(tài)遷移轉(zhuǎn)換上。
5 結(jié)論
目前AADL 已經(jīng)廣泛應(yīng)用到嵌入式系統(tǒng)的開發(fā)中，基于AADL 模型的形式化研究已經(jīng)成為了驗(yàn)證模型可靠性的主要途徑。本文在研究AADL 行為附件的基礎(chǔ)上，建立了AADL 行為模型到BIP 模型的轉(zhuǎn)換規(guī)則。但是由于兩種模型針對的主要描述對象并不完全相同，因此兩者之間有一定差異。在轉(zhuǎn)換中也可能將一些語義，性質(zhì)丟失。例如這種轉(zhuǎn)換對任務(wù)執(zhí)行協(xié)議，執(zhí)行的條件變量等描述不夠。這還需要一些輔助的形式化分析進(jìn)行補(bǔ)充。因此，在對AADL 行為的形式化描述中我們還需要進(jìn)一步完善。這將對提高實(shí)時(shí)關(guān)鍵系統(tǒng)開發(fā)效率，保證系統(tǒng)安全具有重大意義。
【淺析基于BIP 的AADL 行為模型驗(yàn)證方法的論文】相關(guān)文章：
基于SCOSM自適應(yīng)教學(xué)模型設(shè)計(jì)論文07-12
關(guān)于解析基于農(nóng)村電網(wǎng)規(guī)劃綜合降損技術(shù)模型論文報(bào)告07-12
淺析抽象油畫色調(diào)論文07-27
淺析信息寫作方法01-28
淺析意象油畫的語言特征論文07-27
淺析綿竹年畫的色彩特征論文07-27
淺析《長恨歌》主題論文04-15
小貓行為的議論文03-22
應(yīng)對孩子害羞行為的方法04-30