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 model checker Kronos and the probabilistic model checker Prism. The system is modelled as a probabilistic timed automaton. We first use Kronos to perform a symbolic forwards 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 probability of a leader being elected before a deadline, for different deadlines, and study how this minimal probability is influenced by using a biased coin and considering different wire lengths.