基于UPPAAL的DIMA组合可调度分析方法  

Compositional Schedulability Analysis Method for DIMA Based on UPPAAL

作　　者：刘晨 杨志斌[1,2] 胡乔乔 周勇 LIU Chen;YANG Zhibin;HU Qiaoqiao;ZHOU Yong(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China;Key Laboratory of Safety-critical Software,Ministry of Industry and Information Technology,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京211106 [2]高安全系统的软件开发与验证技术工信部重点实验室,南京211106

出　　处：《小型微型计算机系统》2024年第12期3063-3072,共10页Journal of Chinese Computer Systems

基　　金：国家自然科学基金项目(62072233)资助;国防基础科研项目(JCKY2020205C006)资助;航空科学基金项目(201919052002)资助;南京航空航天大学科研与实践创新计划项目(xcxjh20221602)资助。

摘　　要：为了满足不断复杂化的机载任务需求,分布式综合化航空电子系统(DIMA)中任务交互行为随之激增,使其任务调度系统的设计与分析难度进一步增加.针对这一问题,提出基于UPPAAL的DIMA组合可调度分析方法.首先,给出基于UPPAAL的DIMA建模方法,包括分区调度、任务、分区间通信、FC网络延迟、多核处理器资源共享等行为建模;其次,给出基于契约的组合可调度分析方法;最后,基于工业界DIMA系统案例验证所提方法的有效性.In order to meet the increasingly complex requirements of airborne tasks,the task interaction behavior in Distributed Integrated Modular Avionics(DIMA)has increased rapidly,which makes the design and analysis of task scheduling system more difficult.To solve this problem,a compositional schedulability analysis method for DIMA based on UPPAAL is proposed.Firstly,the DIMA modeling based on UPPAAL is presented,including behavior modeling of partition scheduling,tasks,inter partition communication,FC network delay,multi-core processor resource sharing,etc.Secondly,a compositional schedulability analysis method based on contract rules is proposed;Finally,the efficacy of the proposed approach has been confirmed through the case study of an DIMA system.

关 键 词：分布式综合化航空电子系统 组合可调度分析 时间自动机 UPPAAL 

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