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

来源：计算机技术与发展杂志2016年第03期北京时间：

作者：孙健;徐敏

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

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