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.

• Type: Conference
• Year: 2007
• Where: B
• Authors: Bill Stoddart, Dominique Cansell, Frank Zeyda
• Keywords: B 2007, Interrupt Driven Scheduler, Interrupt Driven Scheduling, Model, Software Engineering