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 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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alur R, Courcoubetis C, Dill D (1991) Model-checking for probabilistic real-time systems. In: Albert JL, Monien B, Rodríguez-Artalejo M (eds) Proceedings of the international coference on automata, languages and programming (ICALP’91), Madrid, 8–12 July 1991. Lecture notes in computer science, vol 510. Springer, Berlin Heidelberg New York
Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inform Comput 104(1):2–34
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235
Alur R, Henzinger T (1999) Reactive modules. Formal Meth Sys Des 15(1):7–48
Bahar I, Frohm E, Gaona C, Hachtel G, Macii E, Pardo A, Somenzi F (1993) Algebraic decision diagrams and their applications. In: Proceedings of the international conference on computer-aided design (ICCAD’93), Santa Clara, CA, , 7–11 April 1993, pp 188–191. Also available in: (1997) Formal Meth Sys Des 10(2/3):171–206
Baier C, Haverkort B, Hermanns H, Katoen JP (2000) Model checking continuous-time Markov chains by transient analysis. In: Emerson E, Sistla A (eds) Proceedings of the 12th conference on computer aided verification (CAV 2000), Chicago, 15–19 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 358–372
Baier C, Kwiatkowska MZ (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125–155
Bcg‘Min manual page. http://www.inrialpes.fr/vasy/cadp/man/bcg_min.html
Bianco A, de Alfaro L (1995) Model checking of probabilistic and nondeterministic systems. In: Thiagarajan PS (ed) Proceedings of the 15th conference on foundations of software technology and theoretical computer science (FSTTCS’95), Bangalore, India, 18–20 December 1995. Lecture notes in computer science, vol 1026. Springer, Berlin Heidelberg New York, pp 499–513
Clarke E, Fujita M, McGeer P, McMillan K, Yang J, Zhao X (1993) Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. In: Proceedings of the IEEE international workshop on logic synthesis (IWLS’93), Tahoe City, CA, 23–26 May 1993, pp 1–15. Also available in: (1997) Formal Meth Sys Des 10(2/3):149–169
D’Argenio P, Jeannet B, Jensen H, Larsen K (2001) Reachability analysis of probabilistic systems by successive refinements. In: De Alfaro L, Gilmore S (eds) Proceedings of the process algebra and probabilistic methods and performance modeling and verification joint international workshop, PAPM-PROBMIV 2001, Aachen, Germany, 12–14 September 2001. Lecture notes in computer science, vol 2165. Springer, Berlin Heidelberg New York, pp 29–56
D’Argenio P, Jeannet B, Jensen H, Larsen K (2002) Reduction and refinement strategies for probabilistic analysis. In: Hermanns H, Segala R (eds) Proceedings of process algebra and probabilistic methods and performance modeling and verification joint international workshop, PAPM-PROBMIV 2002, Copenhagen, 25–26 July 2002. Lecture notes in computer science, vol 2399. Springer, Berlin Heidelberg New York, pp 57–76
Daws C, Kwiatkowska M, Norman G (2002) Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. In: Proceedings of the 7th international workshop on formal methods for industrial critical systems (FMICS’02), Malaga, Spain, 12–13 July 2002. Electronic notes in theoretical computer science, vol 66(2). Elsevier, Amsterdam
Daws C, Olivero A, Tripakis S, Yovine S (1996) The tool Kronos. In: Alur R, Henzinger TA, Sontag ED (eds) Hybrid systems III: verification and control. Proceedings of the DIMACS/SYCON workshop, New Brunswick, NJ, 22–25 October 1996. Lecture notes in computer science, vol 1066. Springer, Berlin Heidelberg New York, pp 208–219
Daws C, Tripakis S (1998) Model-checking of real-time reachability properties using abstractions. In: Steffen B (ed) Proceedings of tools and algorithms for construction and analysis of systems (TACAS’98), Lisbon, Portugal, 28 March–4 April 1998. Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 313–329
Daws C, Yovine S (1995) Two examples of verification of multirate timed automata with Kronos. In: Burns A, Lee YH, Ramamritham K (eds) Proceedings of the 16th IEEE real-time systems symposium (RTSS’95). IEEE Press, New York, pp 66–75
De Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Baeten J, Mauw S (eds) Proceedings of CONCUR ’99: Concurrency Theory, Eindhoven, The Netherlands, 24–27 August 1999. Lecture notes in computer science, vol 1664. Springer, Berlin Heidelberg New York, pp 66–81
De Alfaro L, Kwiatkowska M, Norman G, Parker D, Segala R (2000) Symbolic model checking of concurrent probabilistic processes using MTBDDs and the Kronecker representation. In: Graf S, Schwartzbach M (eds) Proceedings of tools and algorithms for the construction and analysis of systems (TACAS’00), Berlin, 25 March–2 April 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 395–410
Garavel H, Hermanns H (2002) On combining functional verification and performance evaluation using CADP. In: Eriksson L, Lindsay P (eds) Proceedings of FME 2002: international symposium of formal methods Europe, Copenhagen, 22–24 July 2002. Lecture notes in computer science, vol 2391. Springer, Berlin Heidelberg New York, pp 410–429
Garavel H, Lang F, Mateescu R (2001) An overview of CADP. Technical Report RT-254, INRIA
Hansson H, Jonsson B (1994) A logic for reasoning about time and probability. Formal Aspects Comput 6(5):512–535
Henzinger T, Ho PH, Wong-Toi H (1995) A user guide to HyTech. In: Brinksma E, Cleaveland W, Larsen K, Margaria T, Steffen B (eds) Proceedings of tools and algorithms for the construction and analysis of systems (TACAS’95), Aarhus, Denmark, 19–20 May 1995. Lecture notes in computer science, vol 1019. Springer, Berlin Heidelberg New York, pp 41–71
Henzinger T, Ho PH, Wong-Toi H (1997) HyTech: a model checker for hybrid systems. J Softw Tools Technol Transfer 1(1–2):110–122
Kemeny J, Snell J, Knapp A (1976) Denumerable Markov chains. Graduate texts in mathematics, 2nd edn. Springer, Berlin Heidelberg New York
KRONOS Web page. http://www-verimag.imag.fr/TEMPORISE/kronos/
Kwiatkowska M, Norman G, Parker D (2002) PRISM: Probabilistic symbolic model checker. In: Field JBT, Harrison P, Bradley J, Harder U (eds) Proceedings of modelling techniques and tools for computer performance evaluation (TOOLS’02), London, 14–17 April 2002. Lecture notes in computer science, vol 2324. Springer, Berlin Heidelberg New York, pp 200–204
Kwiatkowska M, Norman G, Parker D (2002) Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen JP, Stevens P (eds) Proceedings of tools and algorithms for construction and analysis of systems (TACAS 2002), Grenoble, France, 8–12 April 2002. Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 52–66
Kwiatkowska M, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282:101–150. A preliminary version of this paper appeared in: Proceedings of ARTS’99, Bamberg, Germany, 26–28 May 1999. Lecture notes in computer science, vol 1601. Springer, Berlin Heidelberg New York, pp 75–95
Kwiatkowska M, Norman G, Sproston J (2002) Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects Comput (Special Issue) 14:295–318
Larsen K, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Softw Tools Technol Transfer 1(1+2):134–152
Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inform Comput 94(1):1–28. A preliminary version of this paper appeared in: Proceedings of the 16th annual ACM symposium on principles of programming languages, Austin, TXUSA, 11–13 January 1989, pp 134–352
PRISM Web page. http://www.cs.bham.ac.uk/∼dxp/prism/
Segala R, Lynch N (1995) Probabilistic simulations for probabilistic processes. Nordic J Comput 2(2):250–273
Simons D, Stoelinga M (2001) Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k. Int J Softw Tools Technol Transfer 3(4):469–485
Stoelinga M (2002) Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, Univerisity of Nijmegen, The Netherlands
Vardi M (1985) Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the symposium on the foundations of computer science (FOCS’85), Portland, OR, 21–23 October 1985. IEEE Press, New York
Author information
Authors and Affiliations
Corresponding authors
Rights and permissions
About this article
Cite this article
Daws, C., Kwiatkowska, M. & Norman, G. Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM. STTT 5, 221–236 (2004). https://doi.org/10.1007/s10009-003-0118-5
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-003-0118-5