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 and the probabilistic model-checker Prism. The system is modelled as a probabilistic timed automaton. We first use Kronos to perform a symbolic forward reachability analysis to generate the set of states that are reachable with non-zero probability from the initial state, and before the deadline expires. We then encode this information as a Markov decision process to be analyzed with Prism. We apply this technique to compute the minimal probabiliy of a leader being elected before a deadline, for different deadlines, and study the influence of using a biased coin on this minimal probability. Key words: model checking, soft deadlines, probabilistic timed automata, IEEE 1394, root contention protocol

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Conrado Daws, Marta Z. Kwiatkowska, Gethin Norman
• Keywords: ENTCS 2002, IEEE 1394, Probabilistic, Root Contention Protocol