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.
@article{arxiv.2012.01493,
title = {A Rely-Guarantee Specification of Mixed-Criticality Scheduling},
author = {Cliff B Jones and Alan Burns},
journal= {arXiv preprint arXiv:2012.01493},
year = {2022}
}
Comments
This paper will appear in a Festschrift - on publication we will insert a pointer to the book