The architecture of ARINC-653 partitioned scheduling has been widely applied to avionics systems owing to its robust temporal isolation among applications. However, this partitioning mechanism causes the problem of how to optimize the partition scheduling of a complex system while guaranteeing its schedulability. In this paper, a model-based optimization approach is proposed. We formulate the problem as a parameter sweep application, which searches for the optimal partition scheduling parameters with respect to minimum processor occupancy via an evolutionary algorithm. An ARINC-653 partitioned scheduling system is modeled as a set of timed automata in the model checker UPPAAL. The optimizer tentatively assigns parameter settings to the models and subsequently invokes UPPAAL to verify schedulability as well as evaluate promising solutions. The parameter space is explored with an evolutionary algorithm that combines refined genetic operators and the self-adaptation of evolution strategies. The experimental results show the applicability of our optimization method.

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.

ARINC 653 Part 1 Supplement 5 (ARINC 653P1-5) provides temporal partitioning capabilities for real-time applications running on the multicore processors in Integrated Modular Avionics (IMAs) systems. However, it is difficult to schedule a set of ARINC 653 multicore partitions to achieve a minimum processor occupancy. This paper proposes a model-based optimization method for ARINC 653 multicore partition scheduling. The IMA multicore processing system is modeled as a network of timed automata in UPPAAL. A parallel genetic algorithm is employed to explore the solution space of the IMA system. Owing to a lack of priori information for the system model, the configuration of genetic operators is self-adaptively controlled by a Q-learning algorithm. During the evolution, each individual in a population is evaluated independently by compositional model checking, which verifies each partition in the IMA system and combines all the schedulability results to form a global fitness evaluation. The experiments show that our model-based method outperforms the traditional analytical methods when handling the same task loads in the ARINC 653 multicore partitions, while alleviating the state space explosion of model checking via parallelization acceleration.

This work presents a compositional approach for schedulability analysis of Distributed Integrated Modular Avionics (DIMA) systems that consist of spatially distributed ARINC-653 modules connected by a unified AFDX network. We model a DIMA system as a set of stopwatch automata in UPPAAL to verify its schedulability by model checking. However, direct model checking is infeasible due to the large state space. Therefore, we introduce the compositional analysis that checks each partition including its communication environment individually. Based on a notion of message interfaces, a number of message sender automata are built to model the environment for a partition. We define a timed selection simulation relation, which supports the construction of composite message interfaces. By using assume-guarantee reasoning, we ensure that each task meets the deadline and that communication constraints are also fulfilled globally. The approach is applied to the analysis of a concrete DIMA system.

This paper presents a modeling framework for schedulability analysis of distributed integrated modular avionics (DIMA) systems that consist of spatially distributed ARINC-653 modules connected by a unified AFDX network. We model a DIMA system as a set of stopwatch automata (SWA) in UPPAAL to analyze its schedulability by classical model checking (MC) and statistical model checking (SMC). The framework has been designed to enable three types of analysis: global SMC, global MC, and compositional MC. This allows an effective methodology including (1) quick schedulability falsification using global SMC analysis, (2) direct schedulability proofs using global MC analysis in simple cases, and (3) strict schedulability proofs using compositional MC analysis for larger state space. The framework is applied to the analysis of a concrete DIMA system.

In the Interval Job Shop Problem (IJSP), operation processing times are represented by intervals, making machine-sequencing decisions sensitive to temporal uncertainty. We propose Risk-Aware Partial-Order Reinforcement Learning with Timed Automata Completion (RAPO-RL-TAC), which couples Risk-Aware Partial-Order Reinforcement Learning (RAPO-RL) for machine-order construction with Timed Automata Completion (TAC) for execution-time resolution of deferred sequencing decisions. Risk awareness focuses on preserving temporal flexibility in machine-order relations whose preferred ordering is sensitive to interval uncertainty. RAPO-RL selectively commits comparatively determinate machine conflicts while retaining a bounded set of timing-sensitive relations. TAC completes unresolved relations as execution evolves, while statistical model checking characterises completion-time variability across timed executions. On 14 ORB and LA benchmark instances, RAPO-RL-TAC achieves mean midpoint makespans 2.92% and 1.63% lower than population-based neighbourhood search (PNS) and genetic algorithm (GA), respectively. Compared with reproduced Fast Elitist Artificial Bee Colony (fEABC) variants, RAPO-RL-TAC achieves a lower midpoint than at least one variant on 7 of 14 instances. In the controlled ablation study, RAPO-RL-TAC achieves a 13.85% lower mean midpoint makespan than hard enforcement of the learned relations. These results indicate that risk-aware selective commitment preserves temporal flexibility while maintaining competitive nominal schedule quality under interval uncertainty.