ARINC653实时任务可调度性验证方法

Method for Verifying ARINC653 Real-time Task Schedulability

针对综合模块化航空电子系统(Integrated Modular Avionics,IMA)存在周期任务和非周期任务,以及任务间依赖关系,传统方法不能准确验证其实时任务可调度性的问题,本文提出了一种基于Stopwatch时间自动机的ARINC653实时任务可调度性验证方法,利用模型检验工具UPPAAL对IMA系统进行建模仿真,并结合统计模型检验(Statistical Model Checking,SMC)与符号模型检验(Symbolic Model Checking,MC)来验证其可调度性。实验结果表明,该方法不仅快速验证了IMA系统的可调度性,而且能够准确定位不可调度任务。

In view of the fact that Integrated Modular Avionics(IMA)system has periodic tasks,non-periodic tasks and inter-task depedencies,traditional methods cannot accurately verify the schedulability of real-time tasks,this paper proposes a ARINC653 real-time system task schedulability verification method based on Stopwatch automata,which uses model checking tool UPPAAL to model and simulate ARINC653 real-time system,and combines statistical model checking(SMC)and symbolic model checking(MC)to verify its schedulability.Experiments demonstrate that the proposed method can not only verify the schedulability of IMA system quickly,but also locate the non-schedulable tasks accurately.