A formal approach to design and verification of two-level Hierarchical Scheduling systems

Hierarchical scheduling (HS) systems manage a set of real-time applications through a scheduling hierarchy, enabling partitioning and reduction of complexity, confinement of failure modes, and separation of concerns. This plays a crucial role in all industrial areas where high-performance microprocessors allow growing integration of multiple applications on a single platform. In this paper, we propose a methodology for formal specification and schedulability analysis of HS systems with complex task-sets and non-deterministic temporal parameters. This exploits the theory of preemptive Time Petri Nets (pTPNs) and takes advantage of the temporal isolation induced by a Time Division Multiplexing (TDM) global scheduler to cope with the problem of state space explosion. We then describe the way how the formal specification can be implemented on top of RTAI operating system, and we report on a testing approach to the verification of its conformance with respect to concurrency and timing semantics of the pTPN design model.