Sciweavers

ISOLA
2007
Springer

Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method

14 years 16 days ago
Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method
We present a model of the IEEE 1394 Root Contention Protocol with a proof of Safety. This model has real-time properties which are expressed in the language of the event B method: first-order classical logic and set theory. Verification is done by proof using the event B method and its prover, we also have a way to model-check models. Refinement is used to describe the system at different levels of abstraction: first without time to fix the scheduling of events abstracly, and then with more and more time constraints. Keywords Formal method · Real-time · Event-B method · Theorem proving
Joris Rehm, Dominique Cansell
Added 08 Jun 2010
Updated 08 Jun 2010
Type Conference
Year 2007
Where ISOLA
Authors Joris Rehm, Dominique Cansell
Comments (0)