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.

• Type: Journal
• Year: 2010
• Where: STTT
• Authors: Joris Rehm
• Keywords: Contention Protocol, First-order Classical Logic, Ieee 1394 Root, Software Engineering, STTT 2010