A Rely-Guarantee Specification of Mixed-Criticality Scheduling

TL;DR

This paper introduces a rely-guarantee formal framework for mixed-criticality scheduling, incorporating resilience to overruns and a novel model for hardware clock time approximation.

Contribution

It presents a layered formal approach using Rely-Guarantee conditions and the Timeband framework, with a new model linking actual and hardware clock time.

Findings

Layered scheduling description with resilience features

Formal modeling of hardware clock time approximation

Application of Rely-Guarantee conditions to mixed-criticality scheduling

Abstract

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.