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

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