Sciweavers

ENTCS
2002
139views more  ENTCS 2002»
13 years 11 months ago
Automatic Verification of the IEEE-1394 Root Contention Protocol with KRONOS and PRISM
We report on the automatic verification of timed probabilistic properties of the IEEE 1394 root contention protocol combining two existing tools: the real-time modelchecker Kronos...
Conrado Daws, Marta Z. Kwiatkowska, Gethin Norman
ENTCS
2000
63views more  ENTCS 2000»
13 years 11 months ago
The Leader Election Protocol of IEEE 1394 in Maude
In this paper we consider two descriptions in Maude of the leader election protocol from the IEEE 1394 serial multimedia bus. Particularly, the time aspects of the protocol are st...
Alberto Verdejo, Isabel Pita, Narciso Martí...
B
2007
Springer
14 years 5 months ago
Time Constraint Patterns for Event B Development
Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the cu...
Dominique Cansell, Dominique Méry, Joris Re...