【摘要】：AADL(Architecture Analysis and Design Language)是一種用于描述復雜嵌入式系統(tǒng)體系架構(gòu)的建模語言國際標準,被廣泛用于安全關(guān)鍵系統(tǒng)的建模與驗證。AADL通過系統(tǒng)、子系統(tǒng)、進程、線程等組件層次化地表達系統(tǒng)模型。行為附件(Behavior Annex)是AADL在功能行為方面的補充,它通過扁平狀態(tài)機的形式對組件的內(nèi)部功能行為以及組件和組件間的交互行為建模。工業(yè)界中的復雜系統(tǒng)常使用層次狀態(tài)機描述組件的功能行為。但是,行為附件中沒有表達層次狀態(tài)機的機制,雖然可以利用AADL自身的分層描述能力對系統(tǒng)建模,但會導致線程的規(guī)模過于龐大。在實際的開發(fā)過程中,設(shè)計者們往往需要將層次化描述的功能需求進行手動扁平化處理,然后借助AADL行為附件對其建模,這個過程是繁瑣的且易錯的,并且扁平化的狀態(tài)機會造成結(jié)構(gòu)信息的丟失,無法直觀的表示功能行為模塊的包含層次關(guān)系。針對AADL行為附件不能以層次化的形式建模功能行為這一問題,本文提出了一種基于AADL行為附件的功能行為層次化建模及驗證方法,包括基于擴展的AADL層次行為附件建模方法和層次行為附件的形式化驗證方法兩部分。為了適應(yīng)工業(yè)界的實際建模需求,本文首先提出了AADL行為附件的層次化擴展——層次行為附件HBA,給出了HBA的形式語法,定義了HBA的操作語義,提出了HBA的元模型,并在OSATE環(huán)境中實現(xiàn)其文本和圖形化編輯器。為了對所建模型進行形式化驗證,本文提出了層次行為附件的形式化驗證方法。首先通過層次行為附件扁平化方法將層次行為模型轉(zhuǎn)化為多個相關(guān)聯(lián)的扁平狀態(tài)機,然后通過層次行為附件到時間自動機的轉(zhuǎn)換方法將層次行為模型轉(zhuǎn)換為時間自動機網(wǎng)絡(luò),最后人工抽取與被驗?zāi)Ｐ拖嚓P(guān)屬性,并將待驗證模型與待驗證屬性輸入到UPPAAL中,對所建模型進行驗證。最后,通過一個航天器導航、制導與控制系統(tǒng)案例來驗證本文所提方法的有效性。首先通過詳細描述建模過程、逐步精化原始需求的方式,檢驗本文所提建模方法是否適用于建模實際工業(yè)案例;然后通過在原始需求中預(yù)埋錯誤的方式,檢驗本文所提出的HBA形式化驗證方法是否可以檢測出所建模型與待驗證屬性存在不一致的問題。
【圖文】：

第二章 基于 AADL 行為附件的功能行為層次化建模及驗證方法2.1 AADL 語言及 AADL 行為附件概述2.1.1 AADL 概述為了支持復雜嵌入式實時系統(tǒng)建模與分析，2004 年，美國汽車工程師協(xié)會正式發(fā)布架構(gòu)分析與設(shè)計語言 AADL。AADL 是一種專為嵌入式實時系統(tǒng)建模而設(shè)計的架構(gòu)描述語言，它支持高度可演化系統(tǒng)的開發(fā)，系統(tǒng)架構(gòu)的早期分析，以及用于整個生命周期持續(xù)分析的架構(gòu)模型的演變。AADL 采用半形式化的建模概念，描述了嵌入式實時系統(tǒng)的軟件架構(gòu)、硬件架構(gòu)和非功能屬性。AADL 通過組件(component)、連接(connection)等概念描述系統(tǒng)的軟、硬件體系結(jié)構(gòu)；通過特征(feature)和屬性(property)描述系統(tǒng)的功能性質(zhì)與非功能性質(zhì)；通過模式變換描述系統(tǒng)運行時體系結(jié)構(gòu)的變化；通過委員會認證的附件(Annex)以及用戶自定義的屬性集(Property Set)支持擴展；對于建立復雜系統(tǒng)模型，AADL 以包(package)的形式進行分隔與組織[43]。AADL 提供兩種建模方式：文本建模與圖形化建模，如圖 2.1 所示，本文以汽艇自動駕駛儀(PBA)系統(tǒng) AADL模型為例，介紹 AADL 的基本建模元素。

面向功能行為層次化建模的 AADL 行為附件擴展及驗證方法位置（狀態(tài)）沒有遷移。 位置遷移：由于滿足遷移條件而發(fā)生的改變。g , a ,ul l ，即滿足 g 時，，時的位置（狀態(tài)）由 l 遷移到了l ，且f I (l )，f I (l )。上述語義，一個時間自動機的遷移過程可以被簡化為 l , g , a , u ,l E，其中u U 。圖 4.8 給出了一個時間自動機的狀態(tài)遷移示例，在左圖中，gd 為遷移條號（發(fā)送）,ud 為遷移更新。右圖表示當時鐘 cl 大于 10 且接收到同步信號 s從 S3 狀態(tài)變遷為 S4 狀態(tài)，同時給變量 x 賦值為 0。
【學位授予單位】：南京航空航天大學
【學位級別】：碩士
【學位授予年份】：2019
【分類號】：TP368.1

【相似文獻】

相關(guān)期刊論文 前10條

1 覃華;張立臣;;基于AADL的智能交通系統(tǒng)面向方面建模[J];計算機工程與設(shè)計;2017年01期

2 馬錚;周海鷹;黃連麗;陶冰冰;;基于AADL的汽車車身控制模塊可調(diào)度性分析[J];湖北汽車工業(yè)學院學報;2016年03期

3 殷鋒社;湯小明;;基于AADL的航空電子系統(tǒng)的建模研究[J];艦船電子工程;2013年04期

4 成靜;朱怡安;屈華敏;羅文波;江葉春;張濤;;一種基于AADL錯誤模型的軟件安全性分析技術(shù)研究[J];西北工業(yè)大學學報;2014年06期

5 余晃晶;李仁發(fā);黃麗達;;基于AADL的汽車防滑控制系統(tǒng)可調(diào)度性分析[J];湖南大學學報(自然科學版);2012年03期

6 李振松;蔣志雄;顧斌;;AADL模式轉(zhuǎn)換設(shè)計方法研究[J];計算機工程與設(shè)計;2011年12期

7 楊雨婷;張建偉;王泊涵;柯文俊;;基于AADL的民用無人機飛控軟件時間/堆棧分析[J];計算機工程與設(shè)計;2017年10期

8 湯小明;蘇羅輝;宋科璞;;飛行管理系統(tǒng)AADL建模與分析[J];計算機技術(shù)與發(fā)展;2010年03期

9 劉倩;桂盛霖;李允;羅蕾;;基于UPPAAL的AADL模型可調(diào)度性驗證[J];計算機應(yīng)用;2009年07期

10 孫雅晴;穆建成;馬連川;曹源;;基于AADL和Simulink的列控系統(tǒng)雙機熱備結(jié)構(gòu)設(shè)計[J];中國鐵路;2011年09期

相關(guān)會議論文 前2條

1 喻蓉;趙忠文;;基于MDE的異構(gòu)模型的轉(zhuǎn)換研究:AADL到Fiacre[A];第八屆全國信號和智能信息處理與應(yīng)用學術(shù)會議會刊[C];2014年

2 郭鵬;李亞暉;李姣潔;王思凡;;一種機載嵌入式系統(tǒng)資源建模與分析技術(shù)[A];第八屆中國航空學會青年科技論壇論文集[C];2018年

相關(guān)碩士學位論文 前10條

1 許金淼;面向功能行為層次化建模的AADL行為附件擴展及驗證方法[D];南京航空航天大學;2019年

2 劉承威;面向安全關(guān)鍵軟件的AADL設(shè)計模型生成方法[D];南京航空航天大學;2019年

3 楊陽;基于AADL的車用嵌入式實時系統(tǒng)建模方法研究[D];湖南大學;2012年

4 高志偉;基于AADL的嵌入式軟件可靠性建模與評估[D];西安電子科技大學;2011年

5 駱偉;采用AADL建模的日志分析技術(shù)研究與支撐工具設(shè)計[D];湖南大學;2012年

6 羅增;一種基于AADL語言的移動軟件能耗評估方法[D];福建師范大學;2015年

7 劉瑋;AADL模型轉(zhuǎn)換與驗證研究[D];陜西師范大學;2013年

8 劉倩;AADL模型可調(diào)度性分析工具設(shè)計與實現(xiàn)[D];西南交通大學;2010年

9 盧鑫;一種AADL建模工具的設(shè)計與實現(xiàn)[D];華中師范大學;2016年

10 劉維維;基于AADL的嵌入式軟件可靠性建模與評估技術(shù)研究[D];南京航空航天大學;2017年

本文編號：2601920