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

Joris Rehm (1) , Dominique Cansell (1)

1 MOSEL - Proof-oriented development of computer-based systems

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 system at different levels of abstraction: first without time to fix the scheduling of events abstracly, and then with more and more time constraints.

Domaines: Logique en informatique [cs.LO]; Réseaux et télécommunications [cs.NI]

Joris Rehm, Dominique Cansell. Proved Development of the Real-Time Properties of the IEEE 1394 Root Contention Protocol with the Event B Method. ISoLA 2007 Workshop On Leveraging Applications of Formal Methods, Verification and Validation, Dec 2007, Poitiers-Futuroscope, France. pp.179-190. ⟨hal-00184837⟩