本文選題：結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言 + 時(shí)間自動(dòng)機(jī)模型��； 參考：《東南大學(xué)學(xué)報(bào)(自然科學(xué)版)》2015年06期

【摘要】：采用時(shí)間自動(dòng)機(jī)形式化模型檢驗(yàn)方法建立了結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言(AADL)調(diào)度模型的自動(dòng)機(jī),實(shí)現(xiàn)了從AADL模型到時(shí)間自動(dòng)機(jī)模型的自動(dòng)轉(zhuǎn)換與驗(yàn)證.首先,設(shè)計(jì)了周期、非周期的線程時(shí)間自動(dòng)機(jī)模板及搶占、非可搶占的調(diào)度器時(shí)間自動(dòng)機(jī)模板,建立了AADL調(diào)度模型到時(shí)間自動(dòng)機(jī)模型的語(yǔ)義映射法則.然后,設(shè)計(jì)了自動(dòng)化模型轉(zhuǎn)換插件,并將其集成到OSATE建模工具中,實(shí)現(xiàn)了建模、轉(zhuǎn)換、驗(yàn)證的集成開發(fā)環(huán)境.最后,利用UPPAAL工具對(duì)時(shí)間自動(dòng)機(jī)模型進(jìn)行模擬與驗(yàn)證.仿真實(shí)驗(yàn)結(jié)果表明,所建立的模型轉(zhuǎn)換方法能夠有效、實(shí)時(shí)地將AADL模型轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)模型,并可在UPPAAL中分析原模型的可調(diào)度性.
[Abstract]:The automata of structural analysis and design language (AADL) scheduling model is established by using the formal model test method of time automata, and the automatic conversion and verification of the model from AADL model to time automata is realized. First, a periodic, non periodic thread time automata model board and preemption, non preemptive scheduler time automata are designed. The template has established the semantic mapping rule of the AADL scheduling model to the time automata model. Then, the automatic model conversion plug-in is designed and integrated into the OSATE modeling tool. The integrated development environment for modeling, conversion and verification is realized. Finally, the time automata model is simulated and verified with the UPPAAL tool. Simulation experiment junction is used. The results show that the proposed model conversion method is effective. The AADL model is converted into a timed automata model in real time, and the schedulability of the original model can be analyzed in the UPPAAL.
【作者單位】： 南京航空航天大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院;
【基金】：中央高�；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)資金資助項(xiàng)目(NS2015092)
【分類號(hào)】：TP301.1;TP368.1

【參考文獻(xiàn)】

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

1 符寧;杜承烈;李建良;劉志強(qiáng);彭寒;;AADL分級(jí)調(diào)度模型的分析與驗(yàn)證[J];計(jì)算機(jī)研究與發(fā)展;2015年01期

【二級(jí)參考文獻(xiàn)】

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

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

2 楊志斌;皮磊;胡凱;顧宗華;馬殿富;;復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)與分析語(yǔ)言:AADL[J];軟件學(xué)報(bào);2010年05期

【相似文獻(xiàn)】

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

1 尹傳龍;宋偉;莊雷;;識(shí)別時(shí)間自動(dòng)機(jī)中可加速環(huán)的方法[J];計(jì)算機(jī)工程與設(shè)計(jì);2010年23期

2 支小莉,童維勤,戎璐;時(shí)間自動(dòng)機(jī)的自動(dòng)抽象算法[J];西南交通大學(xué)學(xué)報(bào);2004年05期

3 錢俊彥,趙嶺忠;一種基于時(shí)間自動(dòng)機(jī)的域構(gòu)造方法[J];計(jì)算機(jī)應(yīng)用研究;2005年07期

4 朱維軍;王迤冉;李琳娜;周清雷;;時(shí)間自動(dòng)機(jī)兩種模型的構(gòu)造互模擬研究[J];微電子學(xué)與計(jì)算機(jī);2007年01期

5 周清雷;周顏;趙東明;;對(duì)時(shí)間自動(dòng)機(jī)中時(shí)鐘約束的處理[J];微計(jì)算機(jī)信息;2008年07期

6 吳永剛;陸慧娟;程倬;陳江;;基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)建模及驗(yàn)證[J];計(jì)算機(jī)時(shí)代;2011年06期

7 朱維軍;周清雷;;一種時(shí)間自動(dòng)機(jī)時(shí)鐘離散化算法[J];鄭州大學(xué)學(xué)報(bào)(理學(xué)版);2011年03期

8 陳志輝;;基于時(shí)間自動(dòng)機(jī)的信息物理融合系統(tǒng)建模與驗(yàn)證[J];計(jì)算機(jī)與現(xiàn)代化;2012年10期

9 陳亞;李峭;趙露茜;;時(shí)間自動(dòng)機(jī)流量特性的硬件模擬[J];電光與控制;2013年11期

10 宋煌,鄭麗萍,莊雷,蘇錦祥;時(shí)間自動(dòng)機(jī)與自動(dòng)驗(yàn)證[J];鄭州大學(xué)學(xué)報(bào)(自然科學(xué)版);2001年02期

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

1 ;基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)建模及驗(yàn)證[A];第六屆和諧人機(jī)環(huán)境聯(lián)合學(xué)術(shù)會(huì)議（HHME2010)、第19屆全國(guó)多媒體學(xué)術(shù)會(huì)議（NCMT2010）、第6屆全國(guó)人機(jī)交互學(xué)術(shù)會(huì)議（CHCI2010）、第5屆全國(guó)普適計(jì)算學(xué)術(shù)會(huì)議（PCC2010）論文集[C];2010年

2 高新;臧洌;黃越;;基于分簇和時(shí)間自動(dòng)機(jī)的Ad hoc入侵檢測(cè)方法研究[A];2010通信理論與技術(shù)新發(fā)展——第十五屆全國(guó)青年通信學(xué)術(shù)會(huì)議論文集（下冊(cè)）[C];2010年

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

1 周顏;時(shí)間自動(dòng)機(jī)可達(dá)性檢測(cè)方法研究[D];鄭州大學(xué);2007年

2 李巖;可調(diào)整時(shí)間自動(dòng)機(jī)可達(dá)性算法的研究與實(shí)現(xiàn)[D];上海交通大學(xué);2014年

3 王靜;基于時(shí)間自動(dòng)機(jī)的模型驗(yàn)證理論及應(yīng)用研究[D];鄭州大學(xué);2005年

4 朱維軍;基于時(shí)間自動(dòng)機(jī)若干新模型的研究[D];鄭州大學(xué);2005年

5 孫全勇;時(shí)間自動(dòng)機(jī)及其應(yīng)用研究[D];哈爾濱工程大學(xué);2007年

6 程永江;基于時(shí)間自動(dòng)機(jī)的模型驗(yàn)證技術(shù)[D];鄭州大學(xué);2009年

7 許丹;基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)形式化建模與驗(yàn)證[D];蘇州大學(xué);2007年

8 高冠龍;基于時(shí)間自動(dòng)機(jī)模型驗(yàn)證方法優(yōu)化研究[D];鄭州大學(xué);2006年

9 劉棟;時(shí)間自動(dòng)機(jī)可達(dá)性研究[D];鄭州大學(xué);2004年

10 姬莉霞;基于時(shí)間自動(dòng)機(jī)的實(shí)時(shí)系統(tǒng)規(guī)范驗(yàn)證研究[D];鄭州大學(xué);2004年

，

本文編號(hào)：2082702