Abstract:

A formal analytical and verification method was proposed to solve the schedulability problem of Architecture Analysis and Design Language (AADL) model. It used model checker UPPAAL to model external environment and to verify AADL thread components schedulability under nonpreempt dispatch strategy. Moreover, a tool for models translation from AADL to UPPAAL was implemented. Experiment demonstrates that analyzing and verifying the schedulability of AADL models by UPPAAL is feasible. This method produces more precise results than other informal verification method.

摘要：

针对体系结构分析设计语言(AADL)模型的可调度性验证问题，提出了利用模型检测工具UPPAAL对其线程组件在非抢占型调度策略下的可调度性进行形式化分析和验证的方法，并实现了从AADL模型到UPPAAL中模型的模型转换工具。实验结果证明了通过UPPAAL来分析和验证AADL模型的可调度性问题的可行性。相比其他方法而言，基于形式化理论的本方法的验证结果更加精确。

关键词: AADL模型;UPPAAL;可调度性;非抢占