Model-based partition scheduling of integrated modular avionics systems using genetic algorithm

This paper proposes a model-based method for partition optimization in Integrated Modular Avionics (IMA) systems that comply with the ARINC 653 standard. It is a complex combinatorial optimization problem to schedule a variety of real-time partitions to achieve maximum processor utilization in an IMA system. Our approach effectively utilizes timed automata in UPPAAL to address the modeling challenges posed by the ARINC 653 features, including two-level scheduling, multi-core processors, and both strictly and loosely periodic partitions. A parallel genetic algorithm is employed to explore the scheduling parameter space of the IMA model, accelerating the computationally expensive model-based analysis through parallelization and achieving an optimal solution more efficiently than traditional analytical methods. Furthermore, we propose a compositional framework that allows for the independent verification of each partition while aggregating local results to derive global schedulability properties, thereby mitigating the state space explosion commonly encountered in model checking. Experimental results demonstrate that our method achieves lower processor occupancy and improved optimization performance compared to traditional techniques, thereby enhancing both the practical applicability of partition scheduling in IMA systems and the overall efficiency of real-time system design.