Issue No.05 - May (2013 vol.39)
Laura Carnevali , Università di Firenze
Alessandro Pinzuti , Università di Firenze
Enrico Vicario , Università di Firenze
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2012.54
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 high-performance 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 nondeterministic execution times, encompassing intra-application synchronizations through semaphores and mailboxes and interapplication 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 interapplication constraints. Experimentation illustrates results and validates their applicability on two challenging workloads in the field of safety-critical avionic systems.
Real time systems, Complexity theory, Time division multiplexing, Job shop scheduling, Timing, Resource management, Petri nets, symbolic state-space analysis, Real-time systems, hierarchical scheduling, ARINC-653, time division multiplexing, preemptive fixed priority, compositional verification, preemptive time Petri nets
Laura Carnevali, Alessandro Pinzuti, Enrico Vicario, "Compositional Verification for Hierarchical Scheduling of Real-Time Systems", IEEE Transactions on Software Engineering, vol.39, no. 5, pp. 638-657, May 2013, doi:10.1109/TSE.2012.54