A Model-Based Approach to Optimizing Partition Scheduling of Integrated Modular Avionics Systems

The architecture of Integrated Modular Avionics (IMA) provides airborne software with a robust temporal partitioning mechanism, which achieves the reliable fault containment between avionics applications. However, the partition scheduling of an IMA system is a complex nonlinear non-convex optimization problem, making it difficult to solve the optimal temporal allocation for partitions using traditional analytical methods. This paper presents a model-based approach to optimizing the partition scheduling of IMA systems, whose temporal behavior is modeled as a network of timed automata. Given a system model, the optimizer employs a parallel genetic algorithm to search for the optimal partition resource parameters with respect to minimum processor occupancy. For each promising parameter combination, the schedulability constraints and processor occupancy of the system are precisely evaluated by Classical and Statistical Model Checking (i.e., CMC and SMC), respectively. We also apply SMC hypothesis testing to the fast falsification of non-schedulable solutions, thereby speeding up the schedulability verification based on CMC. Two case studies demonstrate that our proposed approach outperforms classical analytical methods on the processor occupancy of typical IMA systems.