基于时间自动机的嵌入式软件模型可调度性验证

摘要：

　　结构分析与设计语言AADL在工业控制、汽车、航空航天等任务关键和实时领域的嵌入式系统开发中得到了广泛的应用。为在开发早期验证模型的可调度性，提出了AADL模型到时间自动机模型的转换方法，将AADL模型中的调度策略映射到时间自动机模型中的调度模板中去，并给出了执行模型和附件模型的具体转换规则。转换后的模型可在UPPAAL工具中进行模拟和验证，分析原模型的可调度性。最后给出了AADL建模、模型转换和模型验证的全过程，证实了方法的有效性。

关键词： 结构分析与设计语言 时间自动机 模型转换 UPPAAL 可调度性验证

作者: 白海洋 李静 赵娜

作者单位: 南京航空航天大学计算机科学与技术学院,南京 2100161

会议类型: 国内会议

会议名称: 第十一届全国软件与应用学术会议(NASAC2012)

会议地点: 南京

会议语种:中文

页码: 1-8

在线出版日期: 2012-10-20（万方平台首次上网日期，不代表论文的发表时间）