  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.

Software Engineering