1 前言
隨著嵌入式系統(tǒng)越來越多的應(yīng)用在工業(yè)控制、車載電子、航天航空電子等任務(wù)關(guān)鍵和實(shí)時系統(tǒng)，它的復(fù)雜度和性能要求也越來越高。傳統(tǒng)的以代碼為核心的開發(fā)方法逐步從代碼為中心的開發(fā)提前到以模型驅(qū)動開發(fā)為核心。以供在早期對系統(tǒng)進(jìn)行設(shè)計驗(yàn)證，減少不必要的損失。為此，美國汽車工程師協(xié)會在2004 年提出了體系結(jié)構(gòu)建模語言AADL(architecturalanalysis and design language, AADL)，并發(fā)布為SAE AS5506 標(biāo)準(zhǔn)，目的是提供一種標(biāo)準(zhǔn)而又足夠精確的方式，設(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í)時系統(tǒng)建模語言，采用自動機(jī)的方式描述行為，并且支持異構(gòu)構(gòu)件之間的組合。BIP 模型工具能夠用來分析模型和可執(zhí)行代碼。BIP 語言對系統(tǒng)的形式化描述主要由下面三部分組成：
原子構(gòu)件：即帶有行為描述的構(gòu)件，這些行為包含了遷移，空交互和優(yōu)先級。觸發(fā)的遷移包括端口，這些端口帶有動作名稱，可用于端口同步。
連接件：用于描述原子構(gòu)件端口之間可能的交互模式。
優(yōu)先級關(guān)系：用于在幾種可能的交互方式中做選擇，這種選擇需要根據(jù)條件來判斷。條件和原子構(gòu)件整體的狀態(tài)有關(guān)。下面詳細(xì)闡述這個語言的主要特征。
2.1 優(yōu)先權(quán)
在包含多個構(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ò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ù)流和時間流)進(jìn)行交互。AADL 模型中每個構(gòu)件內(nèi)的行為模型相對對立，可以直接映射成BIP 描述的原子構(gòu)件，多個構(gòu)件交互的行為可以映射為BIP 復(fù)合構(gòu)件里多個原子構(gòu)件的交互，從而避免了構(gòu)造自動機(jī)的`積的復(fù)雜過程。
4 關(guān)鍵系統(tǒng)的任務(wù)轉(zhuǎn)換實(shí)例
對于實(shí)時的關(guān)鍵系統(tǒng)，系統(tǒng)里具有更高優(yōu)先級的任務(wù)必須能夠搶占正在執(zhí)行的任務(wù)，并且在任務(wù)執(zhí)行完成后恢復(fù)被搶占任務(wù)的執(zhí)行。這既是系統(tǒng)的實(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 行為模型附件語法來為一個可搶占實(shí)時任務(wù)進(jìn)行建模，然后將這個實(shí)時模型的可搶占執(zhí)行模型轉(zhuǎn)換成BIP 行為模型的狀態(tài)遷移過程，并對BIP 模型進(jìn)行驗(yàn)證。因?yàn)檫w移的條件比較復(fù)發(fā)，對于研究實(shí)時任務(wù)的搶占執(zhí)行不具有普遍一起，所以本文簡化的描述了AADL 狀態(tài)的可搶占執(zhí)行到BIP 模型的轉(zhuǎn)換過程。
4.2 BIP模型驗(yàn)證
對于轉(zhuǎn)換而成的BIP 模型，我們可以用驗(yàn)證工具Aldebaran 進(jìn)行死鎖檢測。這個工具主要是對BIP 模型的結(jié)構(gòu)進(jìn)行分析，它的原理是首先它使用前端引擎來探索BIP 模型的所有運(yùn)行狀態(tài)，并將這些狀態(tài)轉(zhuǎn)換成一個帶標(biāo)記的遷移系統(tǒng)，然后將這個帶標(biāo)記的遷移系統(tǒng)作為作為檢測工具的后端輸入，然后對系統(tǒng)進(jìn)行死鎖檢測。
如果對于具有并發(fā)執(zhí)行或者對執(zhí)行時間嚴(yán)格的狀態(tài)轉(zhuǎn)換，我們可以通過設(shè)置狀態(tài)轉(zhuǎn)化的優(yōu)先級或者在模型端口里加入時間變量。通過其他的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í)時關(guān)鍵系統(tǒng)開發(fā)效率，保證系統(tǒng)安全具有重大意義。
【淺析基于BIP 的AADL 行為模型驗(yàn)證方法的論文】相關(guān)文章：
1.淺析基于可驗(yàn)證計算的可信云計算優(yōu)秀論文
3.淺析基于AutoCAD-VBA 的對象交互式操作方法論文
4.淺析基于云存儲的數(shù)字校園存儲架構(gòu)論文
5.淺析基于云計算的網(wǎng)絡(luò)營銷系統(tǒng)構(gòu)建論文
6.基于心理學(xué)視角淺析網(wǎng)紅現(xiàn)象的論文
7.淺析基于物聯(lián)網(wǎng)時代下包裝設(shè)計形態(tài)論文
本文來源：http://www.nvnqwx.com/shiyongwen/2161007.htm