基于时间自动机的嵌入式系统AADL模型可调度性验证

发布时间：2018-06-29 16:30

  本文选题：结构分析与设计语言 + 时间自动机模型　； 参考：《东南大学学报(自然科学版)》2015年06期

【摘要】：采用时间自动机形式化模型检验方法建立了结构分析与设计语言(AADL)调度模型的自动机,实现了从AADL模型到时间自动机模型的自动转换与验证.首先,设计了周期、非周期的线程时间自动机模板及抢占、非可抢占的调度器时间自动机模板,建立了AADL调度模型到时间自动机模型的语义映射法则.然后,设计了自动化模型转换插件,并将其集成到OSATE建模工具中,实现了建模、转换、验证的集成开发环境.最后,利用UPPAAL工具对时间自动机模型进行模拟与验证.仿真实验结果表明,所建立的模型转换方法能够有效、实时地将AADL模型转换为时间自动机模型,并可在UPPAAL中分析原模型的可调度性.
[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.
【作者单位】： 南京航空航天大学计算机科学与技术学院;
【基金】：中央高校基本科研业务费专项资金资助项目(NS2015092)
【分类号】：TP301.1;TP368.1

【参考文献】

相关期刊论文 前1条

1 符宁;杜承烈;李建良;刘志强;彭寒;;AADL分级调度模型的分析与验证[J];计算机研究与发展;2015年01期

【二级参考文献】

相关期刊论文 前2条

1 刘倩;桂盛霖;李允;罗蕾;;基于UPPAAL的AADL模型可调度性验证[J];计算机应用;2009年07期

2 杨志斌;皮磊;胡凯;顾宗华;马殿富;;复杂嵌入式实时系统体系结构设计与分析语言:AADL[J];软件学报;2010年05期

【相似文献】

相关期刊论文 前10条

1 尹传龙;宋伟;庄雷;;识别时间自动机中可加速环的方法[J];计算机工程与设计;2010年23期

2 支小莉,童维勤,戎璐;时间自动机的自动抽象算法[J];西南交通大学学报;2004年05期

3 钱俊彦,赵岭忠;一种基于时间自动机的域构造方法[J];计算机应用研究;2005年07期

4 朱维军;王迤冉;李琳娜;周清雷;;时间自动机两种模型的构造互模拟研究[J];微电子学与计算机;2007年01期

5 周清雷;周颜;赵东明;;对时间自动机中时钟约束的处理[J];微计算机信息;2008年07期

6 吴永刚;陆慧娟;程倬;陈江;;基于时间自动机的实时系统建模及验证[J];计算机时代;2011年06期

7 朱维军;周清雷;;一种时间自动机时钟离散化算法[J];郑州大学学报(理学版);2011年03期

8 陈志辉;;基于时间自动机的信息物理融合系统建模与验证[J];计算机与现代化;2012年10期

9 陈亚;李峭;赵露茜;;时间自动机流量特性的硬件模拟[J];电光与控制;2013年11期

10 宋煌,郑丽萍,庄雷,苏锦祥;时间自动机与自动验证[J];郑州大学学报(自然科学版);2001年02期

相关会议论文 前2条

1 ;基于时间自动机的实时系统建模及验证[A];第六届和谐人机环境联合学术会议（HHME2010)、第19届全国多媒体学术会议（NCMT2010）、第6届全国人机交互学术会议（CHCI2010）、第5届全国普适计算学术会议（PCC2010）论文集[C];2010年

2 高新;臧洌;黄越;;基于分簇和时间自动机的Ad hoc入侵检测方法研究[A];2010通信理论与技术新发展——第十五届全国青年通信学术会议论文集（下册）[C];2010年

相关硕士学位论文 前10条

1 周颜;时间自动机可达性检测方法研究[D];郑州大学;2007年

2 李岩;可调整时间自动机可达性算法的研究与实现[D];上海交通大学;2014年

3 王静;基于时间自动机的模型验证理论及应用研究[D];郑州大学;2005年

4 朱维军;基于时间自动机若干新模型的研究[D];郑州大学;2005年

5 孙全勇;时间自动机及其应用研究[D];哈尔滨工程大学;2007年

6 程永江;基于时间自动机的模型验证技术[D];郑州大学;2009年

7 许丹;基于时间自动机的实时系统形式化建模与验证[D];苏州大学;2007年

8 高冠龙;基于时间自动机模型验证方法优化研究[D];郑州大学;2006年

9 刘栋;时间自动机可达性研究[D];郑州大学;2004年

10 姬莉霞;基于时间自动机的实时系统规范验证研究[D];郑州大学;2004年

，

本文编号：2082702