基于時間自動機(jī)的AADL端到端流規(guī)約驗證方法

摘要： 體系結(jié)構(gòu)分析及設(shè)計語言(AADL)作為一種標(biāo)準(zhǔn)且直觀的實時系統(tǒng)分析與設(shè)計工具，可以為系統(tǒng)設(shè)計、分析、驗證、自動代碼生成等關(guān)鍵環(huán)節(jié)提供統(tǒng)一的抽象表示。然而，AADL模型采用仿真的驗證方法無法得到精確的端到端延遲驗證結(jié)果，尤其是對于資源動態(tài)分配的實時系統(tǒng)。為解決結(jié)果不精確的問題，可結(jié)合基于系統(tǒng)有窮狀態(tài)空間遍歷的模型檢驗方法。首先，將實時系統(tǒng)AADL模型轉(zhuǎn)換為時間自動機(jī)(TA)模型，... （共10頁）