A Rely-Guarantee Specification of Mixed-Criticality Scheduling

TY - CHAP

T1 - A Rely-Guarantee Specification of Mixed-Criticality Scheduling

AU - Jones, Cliff

AU - Burns, Alan

PY - 2022/5/30

Y1 - 2022/5/30

N2 - 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.

AB - 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.

KW - Mixed Criticality

KW - Formal Methods

UR - https://doi.org/10.48550/arXiv.2012.01493

M3 - Chapter

SN - 9781848903999

T3 - Tribute Series

SP - 61

EP - 76

BT - Mathematical Foundations of Software Engineering: Essays in Honour of Tom Maibaum on the Occasion of his Retirement

A2 - Aguirre, Nazareno

A2 - Cassano, Valentin

A2 - Castro, Pablo

A2 - Demasi, Ramiro

PB - College Publications

ER -