10.3969/j.issn.1673-629X.2016.03.006
基于AADL的嵌入式系统可调度性验证
AADL近年来在嵌入式实时系统领域得到了广泛的应用,相对于其他语言能够更好地描述系统的非功能属性,同时支持系统软硬件建模,在基于模型驱动的开发方法下对系统进行建模和分析,用形式化的方法对系统的相关属性进行验证,从而可以在设计阶段发现错误,对保证系统的安全运行和开发效率的提高有着重要意义。对于验证AADL模型可调度性的问题,文中利用时间自动机理论,根据AADL调度模型和时间自动机模型的语义相似性,将AADL模型转换成时间自动机模型,并设计转换插件,通过Eclipse插件开发技术将其集成到AADL建模与分析工具OSATE中。最后在UP-PAAL工具中对转换后的时间自动机模型进行模拟和验证,利用相关性质验证语句等价地对原模型的可调度性进行验证。
嵌入式系统、体系结构分析设计语言、时间自动机、模型转换、UPPAAL、实时性
26
TP302(计算技术、计算机技术)
国家“973”重点基础研究发展计划项目2014CB744900
2016-05-06(万方平台首次上网日期,不代表论文的发表时间)
共4页
23-26