[DKN02] C. Daws, M. Kwiatkowska and G. Norman. Automatic Verification of the IEEE 1394 Root Contention Protocol with KRONOS and PRISM. In Proc. 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02), volume 66.2 of ENTCS. July 2002. [ps.gz] [pdf] [bib]
Downloads:  ps.gz ps.gz (224 KB)  pdf pdf (309 KB)  bib bib
Notes: Further information and verification results are available from the PRISM web page.

An extended version can be found in [DKN04]. ENTCS is available at www.sciencedirect.com/science/journal/15710661.
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 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.