Sciweavers

STTT
2010

Proved development of the real-time properties of the IEEE 1394 Root Contention Protocol with the event-B method

13 years 5 months 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 studied t different levels of abstraction: first without time to fix the scheduling of events abstracly, and then with more and more time constraints.
Joris Rehm
Added 21 May 2011
Updated 21 May 2011
Type Journal
Year 2010
Where STTT
Authors Joris Rehm
Comments (0)