[發明專利]一種基于AADL模態時間自動機模型的嵌入式軟件測試方法

無效

• 申請號: 201010610279.7
• 申請日: 2010-12-23
• 公開（公告）號: CN102063369A
• 公開（公告）日: 2011-05-18
• 發明（設計）人: 董云衛;張云峰;馬春燕;張凡;周偉超;朱宇峰
• 申請（專利權）人: 西北工業大學
• 主分類號: G06F11/36
• 分類號: G06F11/36
• 代理公司: 西北工業大學專利中心 61204
• 代理人: 王鮮凱

1.一種基于AADL模態時間自動機模型的嵌入式軟件測試方法，其特征在于步驟如下：

步驟1：構建AADL架構模型描述文件的構件樹，以系統構件作為樹的根節點，下一層為子系統構件，依次向下為進程構件、線程構件；以構件的名稱作為構件樹中的每個節點的標識，每個節點包含該構件的模態信息；所述的模態信息包括模態名稱、引起模態轉移的事件、模態轉移的目標模態和系統的初始模態；

步驟2：對步驟1得到的構件樹進行廣度優先遍歷，提取每個節點的當前模態，并存儲至時間自動機六元組<∑，S，S₀，C，I，E>的S集合中，提取到的系統初始模態信息存儲在S₀集合中。其中：S是一個有限的狀態集合，S＝{SOM₁，SOM₂，…，SOM_i}為模態的狀態空間，SOM_i為任一模態；S₀是一個起始狀態集合；∑＝{ep₁，ep₂，…，ep_k}是一個有限事件集合，ep_k是集合中某事件；C是一個有限時鐘集合；I是一個映射，它為S中的每一個狀態SOM_i指定Φ(C)中的某一個時鐘約束；E是一個轉移集合，E＝{e₁，e₂，…，e_k}，e_i表示每條轉移，每條轉移(s，a，δ，λ，s′)表示輸入字符a時，從位置s到s′的一個轉移，δ是定義在時鐘集C上的一個時鐘約束，在位置轉移發生時必須被滿足，λ表示發生位置轉移時被重置的所有時鐘變量的集合，且滿足

步驟3：根據步驟2得到的模態的狀態集合S，將S中父節點的模態向量與它的孩子節點的模態向量作笛卡爾乘積，將得到的模態向量繼續添加到S中，構造完成時間自動機<∑，S，S₀，C，I，E>的狀態集合S；

步驟4：根據步驟1得到的構件樹，再一次對構件樹進行廣度優先遍歷，提取每個節點中引起模態轉移的事件，以向量ep_k(k≥1)表示，并存儲至<∑，S，S₀，C，I，E>中的∑中，∑＝{ep₁，ep₂，…，ep_k}，構造完成時間自動機<∑，S，S₀，C，I，E>的事件集合∑；

步驟5：根據步驟3和步驟4得到的狀態集合S和事件集合∑，按照如下的方法構造時間自動機中的轉移集合E：

廣度優先遍歷步驟1得到的構件樹，提取事件集合中每個事件ep_i(1≤i≤k)的源模態集合M_is＝{SOM_si，…，SOM_sj}和目標模態集合M_it＝{SOM_ti，…，SOM_sj}，得到表示在事件集合ep_i觸發下，模態從M_is轉移到模態M_it的每條轉移e_i＝(M_is，e_pi，_，_，M_it)，轉移集合為E＝{e₁，e₂，…，e_k}其中：對∑中的每個ep_i其轉移函數為e_i＝(M_is，ep_i，_，_，M_it)，Mis⊆S,]]>Mit⊆S;]]>

步驟6：為步驟5得到的轉移集合E增加表示模態轉移的時鐘約束c₁，C＝{c₁}；所述的c₁包括模態轉移發生時離開源模態的時間c11和到達目標模態的時間c₁₂，將c₁作為每條轉移函數的時鐘約束，得到轉移函數e_j＝(M_is，ep_i，c₁，{c₁}，M_it)，所述c₁獲取步驟如下：

步驟a：當源模態下線程間的同步屬性Synchronized_Component為true，c₁₁＝{T₁中線程周期的最小公倍數}，否則c₁₁＝0；

步驟b：當目標模態下線程間的同步屬性Synchronized_Component為true，c₁₂＝{T₂中線程周期的最小公倍數}，否則c₁₂＝0；

步驟c：得到轉移時間記為c₁＝c₁₁+c₁₂；

步驟7：重復步驟6，直到E中的所有模態轉移中都增加了時鐘約束，E＝{e₁，e₂，…，e_k}，得到各個元素都構造完成的時間自動機<∑，S，S₀，C，I，E>，AADL模型到時間自動機模型轉換完畢；

步驟8：根據步驟7得到的時間自動機模型，使用時間自動機模型的實時系統驗證工具UPPAAL驗證AADL模型的模態轉移是否滿足實時性和可達性。