發(fā)布時(shí)間：2017-05-11 13:10

  本文關(guān)鍵詞：基于UPPAAL的嵌入式系統(tǒng)AADL模型實(shí)時(shí)性驗(yàn)證，由筆耕文化傳播整理發(fā)布。

【摘要】：隨著嵌入式系統(tǒng)的規(guī)模、復(fù)雜程度和可靠性需求的不斷提升，模型驅(qū)動(dòng)的體系結(jié)構(gòu)開發(fā)方法已經(jīng)成為復(fù)雜嵌入式系統(tǒng)開發(fā)的主流。體系結(jié)構(gòu)分析與設(shè)計(jì)語言AADL（ArchitectureAnalysisand Design Language, AADL）是嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域模型驅(qū)動(dòng)方法的新標(biāo)準(zhǔn)，在支持系統(tǒng)軟、硬件結(jié)構(gòu)建模的同時(shí)可對(duì)可靠性、實(shí)時(shí)性等非功能屬性的描述，可在模型驅(qū)動(dòng)開發(fā)過程早期的模型建立階段，通過形式化的模型檢驗(yàn)方法對(duì)系統(tǒng)模型的關(guān)鍵屬性進(jìn)行驗(yàn)證，及早發(fā)現(xiàn)設(shè)計(jì)過程中潛在的錯(cuò)誤，對(duì)保障系統(tǒng)實(shí)時(shí)性和提高開發(fā)效率都具有重要的意義。 為了對(duì)AADL模型的可調(diào)度性和數(shù)據(jù)流時(shí)延特性進(jìn)行驗(yàn)證，本文采用時(shí)間自動(dòng)機(jī)形式化模型檢驗(yàn)方法建立了AADL模型中調(diào)度模型和數(shù)據(jù)流的時(shí)間自動(dòng)機(jī)，實(shí)現(xiàn)了從AADL模型到時(shí)間自動(dòng)機(jī)模型的轉(zhuǎn)換和驗(yàn)證工作。在調(diào)度模型時(shí)間自動(dòng)機(jī)的建立中，，設(shè)計(jì)了周期、非周期的線程模板以及搶占和非可搶占的調(diào)度器模板，通過模型轉(zhuǎn)換法則將AADL調(diào)度模型轉(zhuǎn)換到時(shí)間自動(dòng)機(jī)模型。在數(shù)據(jù)流的模型轉(zhuǎn)換中，分別設(shè)計(jì)了單一數(shù)據(jù)流和混合數(shù)據(jù)流到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換方法，混合數(shù)據(jù)流轉(zhuǎn)換得到的時(shí)間自動(dòng)機(jī)可與調(diào)度模型時(shí)間自動(dòng)機(jī)構(gòu)成時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)，實(shí)現(xiàn)了數(shù)據(jù)流與調(diào)度模型的綜合分析與驗(yàn)證。 利用Eclipse的插件開發(fā)技術(shù)，設(shè)計(jì)了自動(dòng)化模型轉(zhuǎn)換插件并將其集成到AADL的建模工具OSATE中，實(shí)現(xiàn)了建模、轉(zhuǎn)換、驗(yàn)證與分析過程的集成開發(fā)環(huán)境。最后利用時(shí)間自動(dòng)機(jī)建模與驗(yàn)證工具UPPAAL對(duì)轉(zhuǎn)換得到的時(shí)間自動(dòng)機(jī)進(jìn)行模擬和驗(yàn)證，等價(jià)地驗(yàn)證原AADL模型的設(shè)計(jì)是否滿足實(shí)時(shí)性要求。測(cè)試數(shù)據(jù)表明，所建立模型轉(zhuǎn)換方法能有效地將AADL模型轉(zhuǎn)換到時(shí)間自動(dòng)機(jī)模型，在UPPAAL中能夠正確地分析原模型的可調(diào)度性和數(shù)據(jù)流時(shí)延特性。
【關(guān)鍵詞】：AADL 時(shí)間自動(dòng)機(jī) 可調(diào)度性 數(shù)據(jù)流時(shí)延 模型轉(zhuǎn)換 UPPAAL
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級(jí)別】：碩士
【學(xué)位授予年份】：2014
【分類號(hào)】：TP368.1
【目錄】：

• 摘要4-5
• ABSTRACT5-6
• 目錄6-9
• 圖表清單9-11
• 注釋表11-12
• 第一章 緒論12-18
• 1.1 研究的背景與意義12-13
• 1.2 國內(nèi)外研究現(xiàn)狀及存在的問題13-15
• 1.2.1 國內(nèi)外研究現(xiàn)狀分析13-14
• 1.2.2 目前研究存在的問題14-15
• 1.3 論文研究內(nèi)容及章節(jié)安排15-18
• 第二章 體系結(jié)構(gòu)分析設(shè)計(jì)語言與時(shí)間自動(dòng)機(jī)18-29
• 2.1 AADL 概述18-22
• 2.1.1 組件19-20
• 2.1.2 端口和連接20
• 2.1.3 語法20-21
• 2.1.4 建模實(shí)例21-22
• 2.2 時(shí)間自動(dòng)機(jī)22-25
• 2.2.1 時(shí)間自動(dòng)機(jī)簡介22
• 2.2.2 時(shí)間自動(dòng)機(jī)理論22-24
• 2.2.3 基于時(shí)間自動(dòng)機(jī)的驗(yàn)證24-25
• 2.3 UPPAAL25-28
• 2.3.1 UPPAAL 的擴(kuò)展元素25-27
• 2.3.2 UPPAAL 中的性質(zhì)驗(yàn)證語句27-28
• 2.4 本章小結(jié)28-29
• 第三章 AADL 調(diào)度模型的轉(zhuǎn)換與驗(yàn)證29-52
• 3.1 引言29-30
• 3.2 AADL 調(diào)度模型到時(shí)間自動(dòng)機(jī)模型的語義映射30-33
• 3.2.1 AADL 調(diào)度模型語義30-31
• 3.2.2 線程執(zhí)行狀態(tài)機(jī)31-32
• 3.2.3 模型轉(zhuǎn)換語義映射32-33
• 3.3 調(diào)度模型時(shí)間自動(dòng)機(jī)設(shè)計(jì)33-46
• 3.3.1 符號(hào)說明34-35
• 3.3.2 非可搶占調(diào)度策略時(shí)間自動(dòng)機(jī)設(shè)計(jì)35-40
• 3.3.3 可搶占調(diào)度策略時(shí)間自動(dòng)機(jī)設(shè)計(jì)40-46
• 3.4 可調(diào)度性驗(yàn)證語句46-47
• 3.5 時(shí)間自動(dòng)機(jī)模型正確性檢驗(yàn)47-48
• 3.6 AADL 調(diào)度模型到時(shí)間自動(dòng)機(jī)模型轉(zhuǎn)換方法48-51
• 3.6.1 調(diào)度模型轉(zhuǎn)換流程48-49
• 3.6.2 線程優(yōu)先級(jí)計(jì)算策略49-50
• 3.6.3 線程組件到線程時(shí)間自動(dòng)機(jī)模板的轉(zhuǎn)換示例50-51
• 3.7 本章小結(jié)51-52
• 第四章 AADL 數(shù)據(jù)流的轉(zhuǎn)換與驗(yàn)證52-62
• 4.1 引言52-53
• 4.2 AADL 數(shù)據(jù)流53-55
• 4.2.1 數(shù)據(jù)流簡介53-54
• 4.2.2 數(shù)據(jù)流的形式化描述54-55
• 4.3 數(shù)據(jù)流到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換55-60
• 4.3.1 單一數(shù)據(jù)流轉(zhuǎn)換方法55-57
• 4.3.2 混合數(shù)據(jù)流轉(zhuǎn)換方法57-60
• 4.4 數(shù)據(jù)流性質(zhì)驗(yàn)證語句60
• 4.5 數(shù)據(jù)流轉(zhuǎn)換方法檢驗(yàn)60-61
• 4.6 本章小結(jié)61-62
• 第五章 模型轉(zhuǎn)換插件的設(shè)計(jì)與系統(tǒng)測(cè)試62-74
• 5.1 引言62
• 5.2 模型轉(zhuǎn)換插件功能設(shè)計(jì)62-64
• 5.3 AADL 模型解析模塊64-66
• 5.3.1 AADL 模型文件分析64-65
• 5.3.2 AADL 對(duì)象模型構(gòu)建65-66
• 5.4 模型轉(zhuǎn)換模塊66
• 5.5 時(shí)間自動(dòng)機(jī)模型生成模塊66-68
• 5.5.1 UPPAAL 模型文件分析67-68
• 5.5.2 時(shí)間自動(dòng)機(jī)對(duì)象模型構(gòu)建及模型文件生成68
• 5.6 插件開發(fā)技術(shù)68-69
• 5.7 模型轉(zhuǎn)換及驗(yàn)證測(cè)試69-73
• 5.7.1 測(cè)試環(huán)境70
• 5.7.2 組合測(cè)試用例70
• 5.7.3 測(cè)試方法70-71
• 5.7.4 測(cè)試結(jié)果實(shí)例展示71-72
• 5.7.5 性能分析72-73
• 5.8 本章小結(jié)73-74
• 第六章 總結(jié)與展望74-75
• 6.1 總結(jié)74
• 6.2 展望74-75
• 參考文獻(xiàn)75-79
• 致謝79-80
• 攻讀碩士學(xué)位期間發(fā)表的學(xué)術(shù)論文80

【參考文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前3條

1 朱雪陽,唐稚松;基于時(shí)序邏輯的軟件體系結(jié)構(gòu)描述語言XYZ/ADL[J];軟件學(xué)報(bào);2003年04期

2 王永吉,陳秋萍;單調(diào)速率及其擴(kuò)展算法的可調(diào)度性判定[J];軟件學(xué)報(bào);2004年06期

3 程永江;周清雷;;基于uppaal的飛機(jī)著陸控制系統(tǒng)模型驗(yàn)證[J];計(jì)算機(jī)工程與設(shè)計(jì);2009年23期

  本文關(guān)鍵詞：基于UPPAAL的嵌入式系統(tǒng)AADL模型實(shí)時(shí)性驗(yàn)證，由筆耕文化傳播整理發(fā)布。

本文編號(hào)：357313