{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,29]],"date-time":"2024-03-29T15:05:09Z","timestamp":1711724709451},"reference-count":36,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2004,3,1]],"date-time":"2004-03-01T00:00:00Z","timestamp":1078099200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2004,3]]},"DOI":"10.1007\/s10009-003-0118-5","type":"journal-article","created":{"date-parts":[[2004,3,19]],"date-time":"2004-03-19T18:53:20Z","timestamp":1079722400000},"page":"221-236","source":"Crossref","is-referenced-by-count":24,"title":["Automatic verification of the IEEE 1394 root contention protocol with KRONOS and PRISM"],"prefix":"10.1007","volume":"5","author":[{"given":"Conrado","family":"Daws","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2004,3,1]]},"reference":[{"key":"118_CR1","doi-asserted-by":"crossref","unstructured":"Alur R, Courcoubetis C, Dill D (1991) Model-checking for probabilistic real-time systems. In: Albert JL, Monien B, Rodr\u00edguez-Artalejo M (eds) Proceedings of the international coference on automata, languages and programming (ICALP\u201991), Madrid, 8\u201312 July 1991. Lecture notes in computer science, vol 510. Springer, Berlin Heidelberg New York","DOI":"10.1007\/3-540-54233-7_128"},{"key":"118_CR2","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"Alur","year":"1993","unstructured":"Alur R, Courcoubetis C, Dill D (1993) Model-checking in dense real-time. Inform Comput 104(1):2\u201334","journal-title":"Inform Comput"},{"key":"118_CR3","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"Alur","year":"1994","unstructured":"Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183\u2013235","journal-title":"Theor Comput Sci"},{"key":"118_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"Alur","year":"1999","unstructured":"Alur R, Henzinger T (1999) Reactive modules. Formal Meth Sys Des 15(1):7\u201348","journal-title":"Formal Meth Sys Des"},{"key":"118_CR5","doi-asserted-by":"crossref","unstructured":"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\u201993), Santa Clara, CA, , 7\u201311 April 1993, pp 188\u2013191. Also available in: (1997) Formal Meth Sys Des 10(2\/3):171\u2013206","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"118_CR6","doi-asserted-by":"crossref","unstructured":"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\u201319 July 2000. Lecture notes in computer science, vol 1855. Springer, Berlin Heidelberg New York, pp 358\u2013372","DOI":"10.1007\/10722167_28"},{"key":"118_CR7","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"Baier","year":"1998","unstructured":"Baier C, Kwiatkowska MZ (1998) Model checking for a probabilistic branching time logic with fairness. Distrib Comput 11(3):125\u2013155","journal-title":"Distrib Comput"},{"key":"118_CR8","unstructured":"Bcg\u2018Min manual page. http:\/\/www.inrialpes.fr\/vasy\/cadp\/man\/bcg_min.html"},{"key":"118_CR9","doi-asserted-by":"crossref","unstructured":"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\u201995), Bangalore, India, 18\u201320 December 1995. Lecture notes in computer science, vol 1026. Springer, Berlin Heidelberg New York, pp 499\u2013513","DOI":"10.1007\/3-540-60692-0_70"},{"key":"118_CR10","unstructured":"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\u201993), Tahoe City, CA, 23\u201326 May 1993, pp 1\u201315. Also available in: (1997) Formal Meth Sys Des 10(2\/3):149\u2013169"},{"key":"118_CR11","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio 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\u201314 September 2001. Lecture notes in computer science, vol 2165. Springer, Berlin Heidelberg New York, pp 29\u201356","DOI":"10.1007\/3-540-44804-7_3"},{"key":"118_CR12","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio 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\u201326 July 2002. Lecture notes in computer science, vol 2399. Springer, Berlin Heidelberg New York, pp 57\u201376","DOI":"10.1007\/3-540-45605-8_5"},{"key":"118_CR13","doi-asserted-by":"crossref","unstructured":"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\u201902), Malaga, Spain, 12\u201313 July 2002. Electronic notes in theoretical computer science, vol 66(2). Elsevier, Amsterdam","DOI":"10.1016\/S1571-0661(04)80406-7"},{"key":"118_CR14","doi-asserted-by":"crossref","unstructured":"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\u201325 October 1996. Lecture notes in computer science, vol 1066. Springer, Berlin Heidelberg New York, pp 208\u2013219","DOI":"10.1007\/BFb0020947"},{"key":"118_CR15","doi-asserted-by":"crossref","unstructured":"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\u201998), Lisbon, Portugal, 28 March\u20134 April 1998. Lecture notes in computer science, vol 1384. Springer, Berlin Heidelberg New York, pp 313\u2013329","DOI":"10.1007\/BFb0054180"},{"key":"118_CR16","doi-asserted-by":"crossref","unstructured":"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\u201995). IEEE Press, New York, pp 66\u201375","DOI":"10.1109\/REAL.1995.495197"},{"key":"118_CR17","doi-asserted-by":"crossref","unstructured":"De Alfaro L (1999) Computing minimum and maximum reachability times in probabilistic systems. In: Baeten J, Mauw S (eds) Proceedings of CONCUR \u201999: Concurrency Theory, Eindhoven, The Netherlands, 24\u201327 August 1999. Lecture notes in computer science, vol 1664. Springer, Berlin Heidelberg New York, pp 66\u201381","DOI":"10.1007\/3-540-48320-9_7"},{"key":"118_CR18","doi-asserted-by":"crossref","unstructured":"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\u201900), Berlin, 25 March\u20132 April 2000. Lecture notes in computer science, vol 1785. Springer, Berlin Heidelberg New York, pp 395\u2013410","DOI":"10.1007\/3-540-46419-0_27"},{"key":"118_CR19","doi-asserted-by":"crossref","unstructured":"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\u201324 July 2002. Lecture notes in computer science, vol 2391. Springer, Berlin Heidelberg New York, pp 410\u2013429","DOI":"10.1007\/3-540-45614-7_23"},{"key":"118_CR20","unstructured":"Garavel H, Lang F, Mateescu R (2001) An overview of CADP. Technical Report RT-254, INRIA"},{"key":"118_CR21","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"Hansson","year":"1994","unstructured":"Hansson H, Jonsson B (1994) A logic for reasoning about time and probability. Formal Aspects Comput 6(5):512\u2013535","journal-title":"Formal Aspects Comput"},{"key":"118_CR22","doi-asserted-by":"crossref","unstructured":"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\u201995), Aarhus, Denmark, 19\u201320 May 1995. Lecture notes in computer science, vol 1019. Springer, Berlin Heidelberg New York, pp 41\u201371","DOI":"10.1007\/3-540-60630-0_3"},{"issue":"1\u20132","key":"118_CR23","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/s100090050008","volume":"1","author":"T Henzinger","year":"1997","unstructured":"Henzinger T, Ho PH, Wong-Toi H (1997) HyTech: a model checker for hybrid systems. J Softw Tools Technol Transfer 1(1\u20132):110\u2013122","journal-title":"J Softw Tools Technol Transfer"},{"key":"118_CR24","doi-asserted-by":"crossref","unstructured":"Kemeny J, Snell J, Knapp A (1976) Denumerable Markov chains. Graduate texts in mathematics, 2nd edn. Springer, Berlin Heidelberg New York","DOI":"10.1007\/978-1-4684-9455-6"},{"key":"118_CR25","unstructured":"KRONOS Web page. http:\/\/www-verimag.imag.fr\/TEMPORISE\/kronos\/"},{"key":"118_CR26","doi-asserted-by":"crossref","unstructured":"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\u201902), London, 14\u201317 April 2002. Lecture notes in computer science, vol 2324. Springer, Berlin Heidelberg New York, pp 200\u2013204","DOI":"10.1007\/3-540-46029-2_13"},{"key":"118_CR27","doi-asserted-by":"crossref","unstructured":"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\u201312 April 2002. Lecture notes in computer science, vol 2280. Springer, Berlin Heidelberg New York, pp 52\u201366","DOI":"10.1007\/3-540-46002-0_5"},{"key":"118_CR28","first-page":"Proceedings","volume":"in","author":"Kwiatkowska","year":"2002","unstructured":"Kwiatkowska M, Norman G, Segala R, Sproston J (2002) Automatic verification of real-time systems with discrete probability distributions. Theor Comput Sci 282:101\u2013150. A preliminary version of this paper appeared in: Proceedings of ARTS\u201999, Bamberg, Germany, 26\u201328 May 1999. Lecture notes in computer science, vol 1601. Springer, Berlin Heidelberg New York, pp 75\u201395","journal-title":"A preliminary version of this paper appeared"},{"key":"118_CR29","first-page":"295","volume":"Comput","author":"Kwiatkowska","year":"2002","unstructured":"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\u2013318","journal-title":"Formal Aspects"},{"issue":"1+2","key":"118_CR30","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"K Larsen","year":"1997","unstructured":"Larsen K, Pettersson P, Yi W (1997) Uppaal in a nutshell. Int J Softw Tools Technol Transfer 1(1+2):134\u2013152","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"118_CR31","first-page":"Proceedings","volume":"in","author":"Larsen","year":"1991","unstructured":"Larsen K, Skou A (1991) Bisimulation through probabilistic testing. Inform Comput 94(1):1\u201328. A preliminary version of this paper appeared in: Proceedings of the 16th annual ACM symposium on principles of programming languages, Austin, TXUSA, 11\u201313 January 1989, pp 134\u2013352","journal-title":"A preliminary version of this paper appeared"},{"key":"118_CR32","unstructured":"PRISM Web page. http:\/\/www.cs.bham.ac.uk\/\u223cdxp\/prism\/"},{"key":"118_CR33","first-page":"250","volume":"2","author":"Segala","year":"1995","unstructured":"Segala R, Lynch N (1995) Probabilistic simulations for probabilistic processes. Nordic J Comput 2(2):250\u2013273","journal-title":"Nordic J Comput"},{"key":"118_CR34","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s100090100059","volume":"3","author":"Simons","year":"2001","unstructured":"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\u2013485","journal-title":"Int J Softw Tools Technol Transfer"},{"key":"118_CR35","first-page":"verification","volume":"est","author":"Stoelinga","year":"2002","unstructured":"Stoelinga M (2002) Alea jacta est: verification of probabilistic, real-time and parametric systems. PhD thesis, Univerisity of Nijmegen, The Netherlands","journal-title":"Alea jacta"},{"key":"118_CR36","doi-asserted-by":"crossref","unstructured":"Vardi M (1985) Automatic verification of probabilistic concurrent finite-state programs. In: Proceedings of the symposium on the foundations of computer science (FOCS\u201985), Portland, OR, 21\u201323 October 1985. IEEE Press, New York","DOI":"10.1109\/SFCS.1985.12"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0118-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-003-0118-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0118-5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-003-0118-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,31]],"date-time":"2020-03-31T17:56:09Z","timestamp":1585677369000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-003-0118-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,3]]},"references-count":36,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2004,3]]}},"alternative-id":["118"],"URL":"https:\/\/doi.org\/10.1007\/s10009-003-0118-5","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,3]]}}}