基于AADL的嵌入式系统可调度性验证

发布时间：2017-08-31 06:27

  本文关键词：基于AADL的嵌入式系统可调度性验证

  更多相关文章： 嵌入式系统 体系结构分析设计语言 时间自动机 模型转换 UPPAAL 实时性

【摘要】：AADL近年来在嵌入式实时系统领域得到了广泛的应用,相对于其他语言能够更好地描述系统的非功能属性,同时支持系统软硬件建模,在基于模型驱动的开发方法下对系统进行建模和分析,用形式化的方法对系统的相关属性进行验证,从而可以在设计阶段发现错误,对保证系统的安全运行和开发效率的提高有着重要意义。对于验证AADL模型可调度性的问题,文中利用时间自动机理论,根据AADL调度模型和时间自动机模型的语义相似性,将AADL模型转换成时间自动机模型,并设计转换插件,通过Eclipse插件开发技术将其集成到AADL建模与分析工具OSATE中。最后在UPPAAL工具中对转换后的时间自动机模型进行模拟和验证,利用相关性质验证语句等价地对原模型的可调度性进行验证。
【作者单位】： 南京航空航天大学计算机科学与技术学院;
【关键词】： 嵌入式系统 体系结构分析设计语言 时间自动机 模型转换 UPPAAL 实时性
【基金】：国家“973”重点基础研究发展计划项目(2014CB744900)
【分类号】：TP368.1
【正文快照】： 0引言对于安全关键的嵌入式系统来说,系统的非功能属性跟功能属性一样重要,都需要得到满足[1-2]。基于模型驱动的方法可对系统设计和安全性分析采用一致的模型,该模型贯穿整个开发过程[3]。在系统设计阶段,通过对模型分析和验证,发现错误来提高系统的安全性,保证系统能够正常

【相似文献】

中国期刊全文数据库 前10条

1 徐建华;李允;;基于单调速率的可调度性判定改进算法[J];计算机工程;2011年22期

2 牛云;戴冠中;梁亚琳;;基于时间需求迭代和排队模型的开放式实时系统可调度性分析算法研究[J];计算机科学;2009年01期

3 于晓;王家礼;;偏序的周期任务间可调度性判定算法[J];电子测量与仪器学报;2009年04期

4 张永悦;孙瑜;李允;徐建华;;复杂实时系统可调度性判定工具的研究与实现[J];计算机工程;2013年01期

5 郭锐锋;刘娴;丁万夫;李杰;王鸿亮;;回卷恢复模型下容错实时系统的可调度性分析[J];小型微型计算机系统;2013年06期

6 毛羽刚,张拥军,金士尧,胡华平;一种改进的分布强实时系统可调度性分析算法[J];软件学报;2001年02期

7 王高才;李伟;;基于随机模型的软实实时时系统的任务期望可调调度度性[J];控制理论与应用;2012年01期

8 谢拴勤;潘姿君;;实时多任务系统可调度性工程评估方法研究[J];计算机测量与控制;2007年12期

9 李俊,阳富民,卢炎生;一种可行的容错实时系统可调度性分析[J];软件学报;2005年08期

10 陈劲林,杨士元,胡东成;基于确定周期性任务的进程管理及可调度性分析[J];计算机研究与发展;2000年03期

中国重要会议论文全文数据库 前3条

1 周美娇;应启戛;张凤登;萧伟;冯治宝;;带有空闲帧的FIP总线可调度性分析[A];第六届全国信息获取与处理学术会议论文集（3）[C];2008年

2 王宇;侯朝桢;;数字化操控系统中CAN总线的信息可调度性分析[A];《制造业自动化与网络化制造》学术交流会论文集[C];2004年

3 王宇;侯朝桢;;数字化操控系统中CAN总线的信息可调度性分析[A];先进制造技术论坛暨第三届制造业自动化与信息化技术交流会论文集[C];2004年

中国博士学位论文全文数据库 前6条

1 王磊;容错实时系统可调度性分析研究[D];浙江大学;2005年

2 李俊;容错硬实时系统的可调度性分析[D];华中科技大学;2007年

3 窦强;分布式强实时系统中可调度性分析算法的研究[D];国防科学技术大学;2001年

4 姚兴华;资源供需进程演算的证明系统研究[D];华东师范大学;2014年

5 于晓;基于嵌入式Linux的仪器操作系统的研究[D];西安电子科技大学;2009年

6 钱之琳;基于服务的信息物理融合系统可信建模与分析[D];华东理工大学;2014年

中国硕士学位论文全文数据库 前3条

1 王好;基于eM-Plant原油处理过程的可调度性分析[D];广东工业大学;2013年

2 余飞;基于Uppaal的多处理器实时系统的可调度性分析[D];上海交通大学;2011年

3 张永悦;基于仿真的实时系统可调度性分析工具的研究与实现[D];云南师范大学;2014年

，

本文编号：763986