基于体系结构模型的综合化航电分区可调度性验证
|
摘要
分区可调度性验证是影响综合模块化航电系统(IMA)可靠性与安全性的关键问题。为解决现有的模型驱动验证方法难以满足系统整体验证需求或需要繁琐的二次建模的问题,提出一种基于体系结构分析与设计语言(AADL)的IMA分区可调度性验证建模方法。在构建分区静态体系结构模型的基础上,通过AADL行为附件建模描述系统中任务的调度过程。再采用AADL Inspector工具对模型中的任务调度行为进行动态仿真,根据仿真结果即可对IMA分区可调度性进行评估。案例实验表明,该方法能够有效发现分区调度配置信息中的错误。此外,只需一次性建模即可直接完成可调度性验证。与现有方法相比,避免了对AADL模型进行繁琐的二次转化。
Partition schedulability verification is a key issue affecting the reliability and safety of integrated modular avionics system(IMA). Existing model-driven verification methods are difficult to meet the requirements of system verification or the need for cumbersome conversion modeling. To solve this problem, we proposed an IMA partitioning schedulability verification modeling based on AADL. Based on the partition static architecture model, the task scheduling process in the system was described by AADL behavior attachment model. AADL Inspector was used to simulate the task scheduling behavior in the model. According to the simulation results, the IMA partition schedulability could be evaluated. Experiment results show that this method can find errors in the partition configuration information effectively. In addition, the verification can be performed directly with one-time modeling. Compared with the existing methods, it avoids the conversion of the AADL model.
Partition schedulability verification is a key issue affecting the reliability and safety of integrated modular avionics system(IMA). Existing model-driven verification methods are difficult to meet the requirements of system verification or the need for cumbersome conversion modeling. To solve this problem, we proposed an IMA partitioning schedulability verification modeling based on AADL. Based on the partition static architecture model, the task scheduling process in the system was described by AADL behavior attachment model. AADL Inspector was used to simulate the task scheduling behavior in the model. According to the simulation results, the IMA partition schedulability could be evaluated. Experiment results show that this method can find errors in the partition configuration information effectively. In addition, the verification can be performed directly with one-time modeling. Compared with the existing methods, it avoids the conversion of the AADL model.
引文
[1] Hongchun W,Wensheng N.A Review on Key Technologies of the Distributed Integrated Modular Avionics System[J].International Journal of Wireless Information Networks,2018,25(3):358-369.
[2] 郑军,胡军,柯昌博,等.综合模块化航电软件系统测试方法研究综述[J].计算机应用与软件,2012,29(5):163-168.
[3] 崔西宁,沈玉龙,李亚晖.综合化航空电子系统安全技术研究进展[J].计算机应用与软件,2012,29(11):130-136.
[4] Kniga E,Zharinov I,Shukalov A,et al.Reliability Evaluation of Integrated Modular Avionics Computational Structures for Different Hardware Configurations[J].Key Engineering Materials,2016,685:350-354.
[5] Lu H,Zhou Q,Fei Z,et al.Scheduling Based on Interruption Analysis and PSO for Strictly Periodic and Preemptive Partitions in Integrated Modular Avionics[J].IEEE Access,2018,6(99):13523-13540.
[6] Sha L,Abdelzaher T,?rzén K E,et al.Real Time Scheduling Theory:A Historical Perspective[J].Real-Time Systems,2004,28(2/3):101-155.
[7] 谭龙华,杜承烈,雷鑫.ARINC 653分区实时系统的可调度分析[J].航空学报,2015,36(11):3698-3705.
[8] 王运盛,雷航.综合模块化航空电子分区配置启动机制[J].计算机应用,2017,37(6):1808-1813.
[9] 胡军,程桢,马金晶,等.基于模型转换的IMA系统可调度性验证方法[J].南京航空航天大学学报,2015,47(3):403-411.
[10] 王明明,胡军,张维珺,等.基于模型的IMA时间资源配置验证方法研究[J].计算机技术与发展,2018,28(5):38-43.
[11] 杨志斌,皮磊,胡凯,等.复杂嵌入式实时系统体系结构设计与分析语言:AADL[J].软件学报,2010,21(5):899-915.
[12] Wang S,Liu B,Zhang Q.Approach for integrated modular avionics reconfiguration modelling and reliability analysis based on AADL[J].IET Software,2016,10(1):18-25.
[13] 杨雨婷,张建伟,王泊涵,等.基于AADL的民用无人机飞控软件时间/堆栈分析[J].计算机工程与设计,2017,38(10):2703-2711.
[14] Vergnaud T,Pautet L,Kordon F.Using the AADL to Describe Distributed Applications from Middleware to Software Components[J].Lecture Notes in Computer Science,2017,3555:67-78.
[15] 周璇,何锋,熊华钢.时间触发航电系统架构的建模及调度方法[J].计算机工程与设计,2019,40(1):1-7,83.
[16] Johnsen A,Lundqvist K,Pettersson P,et al.Automated Verification of AADL-Specifications Using UPPAAL[C]//IEEE International Symposium on High-assurance Systems Engineering.2012.
[17] 符宁,杜承烈,李建良,等.AADL分级调度模型的分析与验证[J].计算机研究与发展,2015,52(1):167-176.
[18] 刘畅,谷涛,周庆,等.AADL2ECPN模型转换方法及其在IMA上的应用[J].北京航空航天大学学报,2016,42(9):1884-1891.
[2] 郑军,胡军,柯昌博,等.综合模块化航电软件系统测试方法研究综述[J].计算机应用与软件,2012,29(5):163-168.
[3] 崔西宁,沈玉龙,李亚晖.综合化航空电子系统安全技术研究进展[J].计算机应用与软件,2012,29(11):130-136.
[4] Kniga E,Zharinov I,Shukalov A,et al.Reliability Evaluation of Integrated Modular Avionics Computational Structures for Different Hardware Configurations[J].Key Engineering Materials,2016,685:350-354.
[5] Lu H,Zhou Q,Fei Z,et al.Scheduling Based on Interruption Analysis and PSO for Strictly Periodic and Preemptive Partitions in Integrated Modular Avionics[J].IEEE Access,2018,6(99):13523-13540.
[6] Sha L,Abdelzaher T,?rzén K E,et al.Real Time Scheduling Theory:A Historical Perspective[J].Real-Time Systems,2004,28(2/3):101-155.
[7] 谭龙华,杜承烈,雷鑫.ARINC 653分区实时系统的可调度分析[J].航空学报,2015,36(11):3698-3705.
[8] 王运盛,雷航.综合模块化航空电子分区配置启动机制[J].计算机应用,2017,37(6):1808-1813.
[9] 胡军,程桢,马金晶,等.基于模型转换的IMA系统可调度性验证方法[J].南京航空航天大学学报,2015,47(3):403-411.
[10] 王明明,胡军,张维珺,等.基于模型的IMA时间资源配置验证方法研究[J].计算机技术与发展,2018,28(5):38-43.
[11] 杨志斌,皮磊,胡凯,等.复杂嵌入式实时系统体系结构设计与分析语言:AADL[J].软件学报,2010,21(5):899-915.
[12] Wang S,Liu B,Zhang Q.Approach for integrated modular avionics reconfiguration modelling and reliability analysis based on AADL[J].IET Software,2016,10(1):18-25.
[13] 杨雨婷,张建伟,王泊涵,等.基于AADL的民用无人机飞控软件时间/堆栈分析[J].计算机工程与设计,2017,38(10):2703-2711.
[14] Vergnaud T,Pautet L,Kordon F.Using the AADL to Describe Distributed Applications from Middleware to Software Components[J].Lecture Notes in Computer Science,2017,3555:67-78.
[15] 周璇,何锋,熊华钢.时间触发航电系统架构的建模及调度方法[J].计算机工程与设计,2019,40(1):1-7,83.
[16] Johnsen A,Lundqvist K,Pettersson P,et al.Automated Verification of AADL-Specifications Using UPPAAL[C]//IEEE International Symposium on High-assurance Systems Engineering.2012.
[17] 符宁,杜承烈,李建良,等.AADL分级调度模型的分析与验证[J].计算机研究与发展,2015,52(1):167-176.
[18] 刘畅,谷涛,周庆,等.AADL2ECPN模型转换方法及其在IMA上的应用[J].北京航空航天大学学报,2016,42(9):1884-1891.