Extending Rely-Guarantee thinking to handle Real-Time Scheduling

Cliff Jones, Alan Burns

Research output: Contribution to journalArticlepeer-review


The reference point for developing any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee conditions extend the scope of formal development approaches to tackle concurrency. In addition, real-time systems need ways of both requiring progress and relating that progress to some notion of time. This paper extends rely-guarantee ideas to cope with specifications of --and assumptions about-- real-time schedulers. Furthermore it shows how the approach helps identify and specify fault-tolerance aspects of such schedulers by systematically challenging the assumptions.
Original languageEnglish
Number of pages22
JournalFormal Methods in System Design
Publication statusPublished - 30 Nov 2023

Bibliographical note

© The Author(s) 2023


  • Real-Time
  • schedulability analysis

Cite this