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

• 作者: 孙健 徐敏
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 嵌入式系统 体系结构分析设计语言 时间自动机 模型转换 UPPAAL 实时性
• 年，卷（期）: 2016,（3）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 23-26
• 页数: 4页
• 分类号: TP302
• 字数: 4271字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2016.03.006

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	徐敏	南京航空航天大学计算机科学与技术学院	31	222	7.0	14.0
2	孙健	南京航空航天大学计算机科学与技术学院	17	192	6.0	13.0