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