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

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

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

【相似文獻(xiàn)】

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

6 羅增;一種基于AADL語(yǔ)言的移動(dòng)軟件能耗評(píng)估方法[D];福建師范大學(xué);2015年

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

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

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

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

本文編號(hào)：2601920