Modelling and Proof Analysis of Interrupt Driven Scheduling

Bill Stoddart Dominique Cansell 1 Frank Zeyda
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Type de document :
Communication dans un congrès
Jacques Jullian et Olga Kouchnarenko. The 7th International B Conference - B 2007, Jan 2007, Besançon/France, Springer, 4355/2006, pp.155-170, 2007, LNCS. 〈10.1007/11955757_14〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00156871
Contributeur : Dominique Cansell <>
Soumis le : samedi 23 juin 2007 - 10:10:39
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Lien texte intégral

Identifiants

Collections

Citation

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

Partager

Métriques

Consultations de la notice

223