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

摘要：

AADL近年来在嵌入式实时系统领域得到了广泛的应用，相对于其他语言能够更好地描述系统的非功能属性，同时支持系统软硬件建模，在基于模型驱动的开发方法下对系统进行建模和分析，用形式化的方法对系统的相关属性进行验证，从而可以在设计阶段发现错误，对保证系统的安全运行和开发效率的提高有着重要意义。对于验证AADL模型可调度性的问题，文中利用时间自动机理论，根据AADL调度模型和时间自动机模型的语义相似性，将AADL模型转换成时间自动机模型，并设计转换插件，通过Eclipse插件开发技术将其集成到AADL建模与分析工具OSATE中。最后在UP-PAAL工具中对转换后的时间自动机模型进行模拟和验证，利用相关性质验证语句等价地对原模型的可调度性进行验证。

关键词：嵌入式系统、体系结构分析设计语言、时间自动机、模型转换、UPPAAL、实时性

所属期刊栏目：26

分类号：TP302(计算技术、计算机技术)

资助基金：国家“973”重点基础研究发展计划项目2014CB744900

在线出版日期：2016-05-06（万方平台首次上网日期，不代表论文的发表时间）

页数：共4页

页码：23-26