本文選題：結構分析與設計語言 + 時間自動機模型�。� 參考：《東南大學學報(自然科學版)》2015年06期

【摘要】：采用時間自動機形式化模型檢驗方法建立了結構分析與設計語言(AADL)調(diào)度模型的自動機,實現(xiàn)了從AADL模型到時間自動機模型的自動轉(zhuǎn)換與驗證.首先,設計了周期、非周期的線程時間自動機模板及搶占、非可搶占的調(diào)度器時間自動機模板,建立了AADL調(diào)度模型到時間自動機模型的語義映射法則.然后,設計了自動化模型轉(zhuǎn)換插件,并將其集成到OSATE建模工具中,實現(xiàn)了建模、轉(zhuǎn)換、驗證的集成開發(fā)環(huán)境.最后,利用UPPAAL工具對時間自動機模型進行模擬與驗證.仿真實驗結果表明,所建立的模型轉(zhuǎn)換方法能夠有效、實時地將AADL模型轉(zhuǎn)換為時間自動機模型,并可在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.
【作者單位】： 南京航空航天大學計算機科學與技術學院;
【基金】：中央高�；究蒲袠I(yè)務費專項資金資助項目(NS2015092)
【分類號】：TP301.1;TP368.1

【參考文獻】

相關期刊論文 前1條

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

【二級參考文獻】

相關期刊論文 前2條

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

2 楊志斌;皮磊;胡凱;顧宗華;馬殿富;;復雜嵌入式實時系統(tǒng)體系結構設計與分析語言:AADL[J];軟件學報;2010年05期

【相似文獻】

相關期刊論文 前10條

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

2 支小莉,童維勤,戎璐;時間自動機的自動抽象算法[J];西南交通大學學報;2004年05期

3 錢俊彥,趙嶺忠;一種基于時間自動機的域構造方法[J];計算機應用研究;2005年07期

4 朱維軍;王迤冉;李琳娜;周清雷;;時間自動機兩種模型的構造互模擬研究[J];微電子學與計算機;2007年01期

5 周清雷;周顏;趙東明;;對時間自動機中時鐘約束的處理[J];微計算機信息;2008年07期

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

7 朱維軍;周清雷;;一種時間自動機時鐘離散化算法[J];鄭州大學學報(理學版);2011年03期

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

9 陳亞;李峭;趙露茜;;時間自動機流量特性的硬件模擬[J];電光與控制;2013年11期

10 宋煌,鄭麗萍,莊雷,蘇錦祥;時間自動機與自動驗證[J];鄭州大學學報(自然科學版);2001年02期

相關會議論文 前2條

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

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

相關碩士學位論文 前10條

1 周顏;時間自動機可達性檢測方法研究[D];鄭州大學;2007年

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

3 王靜;基于時間自動機的模型驗證理論及應用研究[D];鄭州大學;2005年

4 朱維軍;基于時間自動機若干新模型的研究[D];鄭州大學;2005年

5 孫全勇;時間自動機及其應用研究[D];哈爾濱工程大學;2007年

6 程永江;基于時間自動機的模型驗證技術[D];鄭州大學;2009年

7 許丹;基于時間自動機的實時系統(tǒng)形式化建模與驗證[D];蘇州大學;2007年

8 高冠龍;基于時間自動機模型驗證方法優(yōu)化研究[D];鄭州大學;2006年

9 劉棟;時間自動機可達性研究[D];鄭州大學;2004年

10 姬莉霞;基于時間自動機的實時系統(tǒng)規(guī)范驗證研究[D];鄭州大學;2004年

，

本文編號：2082702