本文關(guān)鍵詞：基于AADL的嵌入式系統(tǒng)可調(diào)度性驗(yàn)證

  更多相關(guān)文章： 嵌入式系統(tǒng) 體系結(jié)構(gòu)分析設(shè)計(jì)語言 時(shí)間自動(dòng)機(jī) 模型轉(zhuǎn)換 UPPAAL 實(shí)時(shí)性

【摘要】：AADL近年來在嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域得到了廣泛的應(yīng)用,相對(duì)于其他語言能夠更好地描述系統(tǒng)的非功能屬性,同時(shí)支持系統(tǒng)軟硬件建模,在基于模型驅(qū)動(dòng)的開發(fā)方法下對(duì)系統(tǒng)進(jìn)行建模和分析,用形式化的方法對(duì)系統(tǒng)的相關(guān)屬性進(jìn)行驗(yàn)證,從而可以在設(shè)計(jì)階段發(fā)現(xiàn)錯(cuò)誤,對(duì)保證系統(tǒng)的安全運(yùn)行和開發(fā)效率的提高有著重要意義。對(duì)于驗(yàn)證AADL模型可調(diào)度性的問題,文中利用時(shí)間自動(dòng)機(jī)理論,根據(jù)AADL調(diào)度模型和時(shí)間自動(dòng)機(jī)模型的語義相似性,將AADL模型轉(zhuǎn)換成時(shí)間自動(dòng)機(jī)模型,并設(shè)計(jì)轉(zhuǎn)換插件,通過Eclipse插件開發(fā)技術(shù)將其集成到AADL建模與分析工具OSATE中。最后在UPPAAL工具中對(duì)轉(zhuǎn)換后的時(shí)間自動(dòng)機(jī)模型進(jìn)行模擬和驗(yàn)證,利用相關(guān)性質(zhì)驗(yàn)證語句等價(jià)地對(duì)原模型的可調(diào)度性進(jìn)行驗(yàn)證。
【作者單位】： 南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;
【關(guān)鍵詞】： 嵌入式系統(tǒng) 體系結(jié)構(gòu)分析設(shè)計(jì)語言 時(shí)間自動(dòng)機(jī) 模型轉(zhuǎn)換 UPPAAL 實(shí)時(shí)性
【基金】：國家“973”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃項(xiàng)目(2014CB744900)
【分類號(hào)】：TP368.1
【正文快照】： 0引言對(duì)于安全關(guān)鍵的嵌入式系統(tǒng)來說,系統(tǒng)的非功能屬性跟功能屬性一樣重要,都需要得到滿足[1-2]�；谀Ｐ万�(qū)動(dòng)的方法可對(duì)系統(tǒng)設(shè)計(jì)和安全性分析采用一致的模型,該模型貫穿整個(gè)開發(fā)過程[3]。在系統(tǒng)設(shè)計(jì)階段,通過對(duì)模型分析和驗(yàn)證,發(fā)現(xiàn)錯(cuò)誤來提高系統(tǒng)的安全性,保證系統(tǒng)能夠正常

【相似文獻(xiàn)】

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

1 徐建華;李允;;基于單調(diào)速率的可調(diào)度性判定改進(jìn)算法[J];計(jì)算機(jī)工程;2011年22期

2 牛云;戴冠中;梁亞琳;;基于時(shí)間需求迭代和排隊(duì)模型的開放式實(shí)時(shí)系統(tǒng)可調(diào)度性分析算法研究[J];計(jì)算機(jī)科學(xué);2009年01期

3 于曉;王家禮;;偏序的周期任務(wù)間可調(diào)度性判定算法[J];電子測量與儀器學(xué)報(bào);2009年04期

4 張永悅;孫瑜;李允;徐建華;;復(fù)雜實(shí)時(shí)系統(tǒng)可調(diào)度性判定工具的研究與實(shí)現(xiàn)[J];計(jì)算機(jī)工程;2013年01期

5 郭銳鋒;劉嫻;丁萬夫;李杰;王鴻亮;;回卷恢復(fù)模型下容錯(cuò)實(shí)時(shí)系統(tǒng)的可調(diào)度性分析[J];小型微型計(jì)算機(jī)系統(tǒng);2013年06期

6 毛羽剛,張擁軍,金士堯,胡華平;一種改進(jìn)的分布強(qiáng)實(shí)時(shí)系統(tǒng)可調(diào)度性分析算法[J];軟件學(xué)報(bào);2001年02期

7 王高才;李偉;;基于隨機(jī)模型的軟實(shí)實(shí)時(shí)時(shí)系統(tǒng)的任務(wù)期望可調(diào)調(diào)度度性[J];控制理論與應(yīng)用;2012年01期

8 謝拴勤;潘姿君;;實(shí)時(shí)多任務(wù)系統(tǒng)可調(diào)度性工程評(píng)估方法研究[J];計(jì)算機(jī)測量與控制;2007年12期

9 李俊,陽富民,盧炎生;一種可行的容錯(cuò)實(shí)時(shí)系統(tǒng)可調(diào)度性分析[J];軟件學(xué)報(bào);2005年08期

10 陳勁林,楊士元,胡東成;基于確定周期性任務(wù)的進(jìn)程管理及可調(diào)度性分析[J];計(jì)算機(jī)研究與發(fā)展;2000年03期

中國重要會(huì)議論文全文數(shù)據(jù)庫 前3條

1 周美嬌;應(yīng)啟戛;張鳳登;蕭偉;馮治寶;;帶有空閑幀的FIP總線可調(diào)度性分析[A];第六屆全國信息獲取與處理學(xué)術(shù)會(huì)議論文集（3）[C];2008年

2 王宇;侯朝楨;;數(shù)字化操控系統(tǒng)中CAN總線的信息可調(diào)度性分析[A];《制造業(yè)自動(dòng)化與網(wǎng)絡(luò)化制造》學(xué)術(shù)交流會(huì)論文集[C];2004年

3 王宇;侯朝楨;;數(shù)字化操控系統(tǒng)中CAN總線的信息可調(diào)度性分析[A];先進(jìn)制造技術(shù)論壇暨第三屆制造業(yè)自動(dòng)化與信息化技術(shù)交流會(huì)論文集[C];2004年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前6條

1 王磊;容錯(cuò)實(shí)時(shí)系統(tǒng)可調(diào)度性分析研究[D];浙江大學(xué);2005年

2 李俊;容錯(cuò)硬實(shí)時(shí)系統(tǒng)的可調(diào)度性分析[D];華中科技大學(xué);2007年

3 竇強(qiáng);分布式強(qiáng)實(shí)時(shí)系統(tǒng)中可調(diào)度性分析算法的研究[D];國防科學(xué)技術(shù)大學(xué);2001年

4 姚興華;資源供需進(jìn)程演算的證明系統(tǒng)研究[D];華東師范大學(xué);2014年

5 于曉;基于嵌入式Linux的儀器操作系統(tǒng)的研究[D];西安電子科技大學(xué);2009年

6 錢之琳;基于服務(wù)的信息物理融合系統(tǒng)可信建模與分析[D];華東理工大學(xué);2014年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前3條

1 王好;基于eM-Plant原油處理過程的可調(diào)度性分析[D];廣東工業(yè)大學(xué);2013年

2 余飛;基于Uppaal的多處理器實(shí)時(shí)系統(tǒng)的可調(diào)度性分析[D];上海交通大學(xué);2011年

3 張永悅;基于仿真的實(shí)時(shí)系統(tǒng)可調(diào)度性分析工具的研究與實(shí)現(xiàn)[D];云南師范大學(xué);2014年

，

本文編號(hào)：763986