Sciweavers

B
2007
Springer

Modelling and Proof Analysis of Interrupt Driven Scheduling

14 years 5 months ago
Modelling and Proof Analysis of Interrupt Driven Scheduling
Following a brief discussion of uniprocessor scheduling in which we argue the case for formal analysis, we describe a distributed Event B model of interrupt driven scheduling. We first consider a model with two executing tasks, presented with the aid of state machine diagrams. We then present a faulty variant of this model which, under particular event timings, may ”drop” an interrupt. We show how the failure to discharge a particular proof obligation leads us to the conceptual error in this model. Finally we generalise the correct model to n tasks, leading to a reduction in proof effort. Key words: Formal Methods, Interrupt Driven Scheduler, Event Calculus.
Bill Stoddart, Dominique Cansell, Frank Zeyda
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where B
Authors Bill Stoddart, Dominique Cansell, Frank Zeyda
Comments (0)