A Rely-Guarantee Specification of Mixed-Criticality Scheduling
This work provides a formal specification for mixed-criticality scheduling, which is critical for safety-critical systems where job overruns can have severe consequences.
This paper addresses mixed-criticality scheduling, focusing on resilience to job overruns. It proposes a layered description of job scheduling using Rely-Guarantee conditions and the Timeband framework, and introduces a novel formal modeling idea to manage the interplay between actual time and hardware clock approximations.
The application considered is mixed-criticality scheduling. The core formal approaches used are Rely-Guarantee conditions and the Timeband framework; these are applied to give a layered description of job scheduling which includes resilience to jobs overrunning their expected execution time. A novel formal modelling idea is proposed to handle the relationship between actual time and its approximation in hardware clocks.