摘要:架構(gòu)分析與設(shè)計(jì)語(yǔ)言(AADL)是一種用于描述復(fù)雜嵌入式系統(tǒng)體系架構(gòu)的建模語(yǔ)言,被廣泛用于安全關(guān)鍵系統(tǒng)建模與驗(yàn)證。AADL通過行為附件以狀態(tài)機(jī)的形式對(duì)組件的內(nèi)部行為建模。工業(yè)界中的復(fù)雜系統(tǒng)常使用層次自動(dòng)機(jī)描述組件的功能行為,而行為附件中沒有表達(dá)層次自動(dòng)機(jī)的機(jī)制。針對(duì)這一問題,提出了AADL行為附件的層次化擴(kuò)展——HBA。首先給出了HBA的形式語(yǔ)法,然后定義了HBA的操作語(yǔ)義。提出了HBA的元模型,并在OSATE環(huán)境中實(shí)現(xiàn)其文本和圖形化編輯器。為了便于形式化驗(yàn)證,給出了HBA到時(shí)間自動(dòng)機(jī)(TA)的轉(zhuǎn)換規(guī)則,并基于模型檢測(cè)工具UPPAAL進(jìn)行形式化驗(yàn)證。最后,給出一個(gè)案例研究來驗(yàn)證所提方法的有效性。
注:因版權(quán)方要求,不能公開全文,如需全文,請(qǐng)咨詢雜志社。
計(jì)算機(jī)科學(xué)與探索雜志, 月刊,本刊重視學(xué)術(shù)導(dǎo)向,堅(jiān)持科學(xué)性、學(xué)術(shù)性、先進(jìn)性、創(chuàng)新性,刊載內(nèi)容涉及的欄目:綜述探索、簡(jiǎn)訊、學(xué)術(shù)研究、專題報(bào)導(dǎo)、專題報(bào)導(dǎo)。等。于2007年經(jīng)新聞總署批準(zhǔn)的正規(guī)刊物。