Modelling, Verification and Synthesis of Two-Tier Hierarchical Fixed-Priority Preemptive Scheduling
- 1 July 2011
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE) in 2011 23rd Euromicro Conference on Real-Time Systems
- p. 172-181
- https://doi.org/10.1109/ecrts.2011.24
Abstract
Hierarchical scheduling has major benefits when it comes to integrating hard real-time applications. One of those benefits is that it gives a clear runtime separation of applications in the time domain. This in turn gives a protection against timing error propagation in between applications. However, these benefits rely on the assumption that the scheduler itself schedules applications correctly according to the scheduling parameters and the chosen scheduling policy. A faulty scheduler can affect all applications in a negative way. Hence, being able to guarantee that the scheduler is correct is of great importance. Therefore, in this paper, we study how properties of hierarchical scheduling can be verified. We model a hierarchically scheduled system using task automata, and we conduct verification with model checking using the Times tool. Further, we generate C-code from the model and we execute the hierarchical scheduler in the Vx Works kernel. The CPU and memory overhead of the modelled scheduler is compared against an equivalent manually coded two-level hierarchical scheduler. We show that the worst-case memory consumption is similar and that there is a considerable difference in CPU overhead.Keywords
This publication has 30 references indexed in Scilit:
- Verifying the Implementation of an Operating System SchedulerPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2009
- Proving Fairness and Implementation Correctness of a Microkernel SchedulerJournal of Automated Reasoning, 2009
- Formal verification of real-time systems with preemptive schedulingReal-Time Systems, 2008
- Modeling and Formal Analysis of Real–Time System via CCSPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2008
- Task automata: Schedulability, decidability and undecidabilityInformation and Computation, 2007
- SIRAPPublished by Association for Computing Machinery (ACM) ,2007
- Theorem Proving Guided Development of Formal Assertions in a Resource-Constrained Scheduler for High-Level SynthesisFormal Methods in System Design, 2001
- An experiment in using RT-LOTOS for the formal specification and verification of a distributed scheduling algorithm in a nuclear power plant monitoring systemPublished by Springer Science and Business Media LLC ,1997
- A theory of timed automataTheoretical Computer Science, 1994
- Scheduling Algorithms for Multiprogramming in a Hard-Real-Time EnvironmentJournal of the ACM, 1973