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

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