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

Method for Verifying ARINC653 Real-time Task Schedulability

作　　者：雷煜靓 胡宁 陈福 崔西宁 Lei Yuliang;Hu Ning;Chen Fu;Cui Xining(AVIC Xi'an Aeronautics Computing Technique Research Institute,Xi’an 710065,China)

机构地区：[1]中国航空工业集团公司西安航空计算技术研究所,西安710065

出　　处：《单片机与嵌入式系统应用》2021年第4期15-20,共6页Microcontrollers & Embedded Systems

基　　金：国防基础科研项目资助(JCKY2016607B006);工信部民机科研(MJ-2017-S-39)。

摘　　要：针对综合模块化航空电子系统(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.

关 键 词：ARINC653 可调度性 秒表时间自动机 统计模型检验 符号模型检验 

分 类 号：TP316[自动化与计算机技术—计算机软件与理论]