This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Compositional Verification for Hierarchical Scheduling of Real-Time Systems
May 2013 (vol. 39 no. 5)
pp. 638-657
Laura Carnevali, Università di Firenze
Alessandro Pinzuti, Università di Firenze
Enrico Vicario, Università di Firenze
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.
Index Terms:
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
Citation:
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
Usage of this product signifies your acceptance of the Terms of Use.