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