Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Modelling and Proof Analysis of Interrupt Driven Scheduling
verfasst von : Bill Stoddart, Dominique Cansell, Frank Zeyda
Erschienen in: B 2007: Formal Specification and Development in B
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.