A Rely-Guarantee Specification of Mixed-Criticality Scheduling

Cliff Jones, Alan Burns

Research output: Chapter in Book/Report/Conference proceedingChapter


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.
Original languageEnglish
Title of host publicationMathematical Foundations of Software Engineering: Essays in Honour of Tom Maibaum on the Occasion of his Retirement
EditorsNazareno Aguirre, Valentin Cassano, Pablo Castro, Ramiro Demasi
PublisherCollege Publications
Number of pages16
ISBN (Print)9781848903999
Publication statusPublished - 30 May 2022

Publication series

NameTribute Series


  • Mixed Criticality
  • Formal Methods

Cite this