Oxford logo
[DKN04] C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. International Journal on Software Tools for Technology Transfer (STTT), 5(2), pages 221-236. March 2004. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (343 KB)  pdf pdf (479 KB)  bib bib
Notes: Further information and verification results are available from the PRISM web page.
Abstract. 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 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 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.