Compositional verification for Hierarchical Scheduling of Real-Time systems

Hierarchical Scheduling (HS) techniques achieve resource partitioning among a set of Real-Time Applications, providing reduction of complexity, confinement of failure modes, and temporal isolation among system applications. This facilitates compositional analysis for architectural verification and plays a crucial role in all industrial areas where highperformance microprocessors allow growing integration of multiple applications on a single platform. We propose a compositional approach to formal specification and schedulability analysis of Real-Time Applications running under a Time Division Multiplexing (TDM) Global Scheduler and preemptive Fixed Priority (FP) Local Schedulers, according to the ARINC-653 standard. As a characterizing trait, each application is made of periodic, sporadic, and jittering tasks with offsets, jitters, and non-deterministic Execution Times, encompassing intra-application synchronizations through semaphores and mailboxes and inter-application communications among periodic tasks through message passing. The approach leverages the assumption of a TDM partitioning to enable compositional design and analysis based on the model of preemptive Time Petri Nets (pTPNs), which is expressly extended with a concept of Required Interface (RI) that specifies the embedding environment of an application through sequencing and timing constraints. This enables exact verification of intra-application constraints and approximate but safe verification of inter-application constraints. Experimentation illustrates results and validates their applicability on two challenging workloads in the field of safety-critical avionic systems.