摘要：架構分析與設計語言(AADL)是一種用于描述復雜嵌入式系統(tǒng)體系架構的建模語言,被廣泛用于安全關鍵系統(tǒng)建模與驗證。AADL通過行為附件以狀態(tài)機的形式對組件的內部行為建模。工業(yè)界中的復雜系統(tǒng)常使用層次自動機描述組件的功能行為,而行為附件中沒有表達層次自動機的機制。針對這一問題,提出了AADL行為附件的層次化擴展——HBA。首先給出了HBA的形式語法,然后定義了HBA的操作語義。提出了HBA的元模型,并在OSATE環(huán)境中實現(xiàn)其文本和圖形化編輯器。為了便于形式化驗證,給出了HBA到時間自動機(TA)的轉換規(guī)則,并基于模型檢測工具UPPAAL進行形式化驗證。最后,給出一個案例研究來驗證所提方法的有效性。