Modelling and Proof Analysis of Interrupt Driven Scheduling

Bill Stoddart , Dominique Cansell (1) , Frank Zeyda

1 MOSEL - Proof-oriented development of computer-based systems

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.

Mots clés: Event Calculus; Formal Methods; Interrupt Driven Scheduler; Event Calculus.

Domaines: Autre [cs.OH]

Bill Stoddart, Dominique Cansell, Frank Zeyda. Modelling and Proof Analysis of Interrupt Driven Scheduling. The 7th International B Conference - B 2007, Jacques Jullian et Olga Kouchnarenko, Jan 2007, Besançon/France, pp.155-170, ⟨10.1007/11955757_14⟩. ⟨inria-00156871⟩