淺析基于BIP 的AADL 行為模型驗證方法的論文

時間：2022-09-18 14:48:41 論文我要投稿

相關推薦

　　1 前言

淺析基于BIP 的AADL 行為模型驗證方法的論文

　　隨著嵌入式系統(tǒng)越來越多的應用在工業(yè)控制、車載電子、航天航空電子等任務關鍵和實時系統(tǒng)，它的復雜度和性能要求也越來越高。傳統(tǒng)的以代碼為核心的開發(fā)方法逐步從代碼為中心的開發(fā)提前到以模型驅(qū)動開發(fā)為核心。以供在早期對系統(tǒng)進行設計驗證，減少不必要的損失。為此，美國汽車工程師協(xié)會在2004 年提出了體系結構建模語言AADL(architecturalanalysis and design language, AADL)，并發(fā)布為SAE AS5506 標準，目的是提供一種標準而又足夠精確的方式，設計與分析嵌入式實時系統(tǒng)的軟、硬件體系結構及功能和非功能性質(zhì)。由于AADL 具有語法簡單、功能強大、可擴展等優(yōu)點，他已經(jīng)逐步成為工業(yè)界事實上的標準。根據(jù)現(xiàn)有的形式化驗證工具的應用情況，本文通過制定映射規(guī)則，將AADL 行為模型直接轉換成BIP 模型。并且利用已有的BIP 模型工具對準換后的BIP 模型進行驗證。提供一種形式化的驗證AADL 行為模型的新途徑，如圖1 所示。

　　2 BIP構件模型

　　BIP(Behavior,Interaction,Priority) 是Verimag 提出的實時系統(tǒng)建模語言，采用自動機的方式描述行為，并且支持異構構件之間的組合。BIP 模型工具能夠用來分析模型和可執(zhí)行代碼。BIP 語言對系統(tǒng)的形式化描述主要由下面三部分組成：

　　原子構件：即帶有行為描述的構件，這些行為包含了遷移，空交互和優(yōu)先級。觸發(fā)的遷移包括端口，這些端口帶有動作名稱，可用于端口同步。

　　連接件：用于描述原子構件端口之間可能的交互模式。

　　優(yōu)先級關系：用于在幾種可能的交互方式中做選擇，這種選擇需要根據(jù)條件來判斷。條件和原子構件整體的狀態(tài)有關。下面詳細闡述這個語言的主要特征。

　　2.1 優(yōu)先權

　　在包含多個構件交互的系統(tǒng)里，優(yōu)先權可以根據(jù)條件來確定所有執(zhí)行交互的優(yōu)先級。因此優(yōu)先權可以通過設置執(zhí)行遷移約束條件來減少系統(tǒng)的非確定性。這些條件是一套規(guī)則，每條規(guī)則都由和條件交互有關的命令對組成。條件是一個與構件交互變量有關的布爾表達式。當條件滿足，所有交互都可執(zhí)行，則優(yōu)先級高的先執(zhí)行。對于靜態(tài)優(yōu)先級，條件可以忽略。規(guī)則也可以擴展為交互組合。例如規(guī)則P1< 的優(yōu)先權高于p 有著比p1|q更高的優(yōu)先權。此外，優(yōu)先權和交互是兼容的，p|q>

　　3 AADL行為模型到BIP模型的轉換規(guī)則

　　AADL 模型轉換主要是建立AADL 模型與目標模型元素的轉換規(guī)則。本文從AADL模型的行為模型出發(fā)，建立其到BIP 模型的轉換規(guī)則。AADL 行為模型用于描述構件內(nèi)部的詳細行為模式，與其他構件通過端口連接等方式形成的流(包括數(shù)據(jù)流和時間流)進行交互。AADL 模型中每個構件內(nèi)的行為模型相對對立，可以直接映射成BIP 描述的原子構件，多個構件交互的行為可以映射為BIP 復合構件里多個原子構件的交互，從而避免了構造自動機的積的復雜過程。

　　4 關鍵系統(tǒng)的任務轉換實例

　　對于實時的關鍵系統(tǒng)，系統(tǒng)里具有更高優(yōu)先級的任務必須能夠搶占正在執(zhí)行的任務，并且在任務執(zhí)行完成后恢復被搶占任務的執(zhí)行。這既是系統(tǒng)的實時要求，又是系統(tǒng)的安全性要求。對于以汽車電子，航空電子，航空控制系統(tǒng)等為代表的實施關鍵系統(tǒng)，必須建立能夠描述任務執(zhí)行的所有可能狀態(tài)，正確的描述系統(tǒng)任務狀態(tài)的遷移過程，對系統(tǒng)執(zhí)行進行分析。

　　4.1 關鍵系統(tǒng)任務的AADL行為描述

　　本文首先用AADL 行為模型附件語法來為一個可搶占實時任務進行建模，然后將這個實時模型的可搶占執(zhí)行模型轉換成BIP 行為模型的狀態(tài)遷移過程，并對BIP 模型進行驗證。因為遷移的條件比較復發(fā)，對于研究實時任務的搶占執(zhí)行不具有普遍一起，所以本文簡化的描述了AADL 狀態(tài)的可搶占執(zhí)行到BIP 模型的轉換過程。

　　4.2 BIP模型驗證

　　對于轉換而成的BIP 模型，我們可以用驗證工具Aldebaran 進行死鎖檢測。這個工具主要是對BIP 模型的結構進行分析，它的原理是首先它使用前端引擎來探索BIP 模型的所有運行狀態(tài)，并將這些狀態(tài)轉換成一個帶標記的遷移系統(tǒng)，然后將這個帶標記的遷移系統(tǒng)作為作為檢測工具的后端輸入，然后對系統(tǒng)進行死鎖檢測。

　　如果對于具有并發(fā)執(zhí)行或者對執(zhí)行時間嚴格的狀態(tài)轉換，我們可以通過設置狀態(tài)轉化的優(yōu)先級或者在模型端口里加入時間變量。通過其他的BIP 模型檢測器來驗證。文獻舉例驗證了構件之間通過端口的同步交互，這種方法可以擴展到對AADL 行為模型的狀態(tài)遷移轉換上。

　　5 結論

　　目前AADL 已經(jīng)廣泛應用到嵌入式系統(tǒng)的開發(fā)中，基于AADL 模型的形式化研究已經(jīng)成為了驗證模型可靠性的主要途徑。本文在研究AADL 行為附件的基礎上，建立了AADL 行為模型到BIP 模型的轉換規(guī)則。但是由于兩種模型針對的主要描述對象并不完全相同，因此兩者之間有一定差異。在轉換中也可能將一些語義，性質(zhì)丟失。例如這種轉換對任務執(zhí)行協(xié)議，執(zhí)行的條件變量等描述不夠。這還需要一些輔助的形式化分析進行補充。因此，在對AADL 行為的形式化描述中我們還需要進一步完善。這將對提高實時關鍵系統(tǒng)開發(fā)效率，保證系統(tǒng)安全具有重大意義。

【淺析基于BIP 的AADL 行為模型驗證方法的論文】相關文章：

基于SCOSM自適應教學模型設計論文07-12

關于解析基于農(nóng)村電網(wǎng)規(guī)劃綜合降損技術模型論文報告07-12

淺析抽象油畫色調(diào)論文07-27

淺析信息寫作方法01-28

淺析鐵路機車的檢修質(zhì)量論文04-14