{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:55:06Z","timestamp":1761807306640,"version":"3.41.0"},"reference-count":27,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2005,3,1]],"date-time":"2005-03-01T00:00:00Z","timestamp":1109635200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGMETRICS Perform. Eval. Rev."],"published-print":{"date-parts":[[2005,3]]},"abstract":"<jats:p>\n            In this paper, we describe some practical applications of\n            <jats:italic>probabilistic model checking,<\/jats:italic>\n            a technique for the formal analysis of systems which exhibit stochastic behaviour. We give an overview of a selection of case studies carried out using the probabilistic model checking tool PRISM, demonstrating the wide range of application domains to which these methods are applicable. We also illustrate several benefits of using formal verification techniques to analyse probabilistic systems, including: (i) that they allow a wide range of numerical properties to be computed accurately; and (ii) that they perform a complete and exhaustive analysis enabling, for example, a study of best- and worst-case scenarios.\n          <\/jats:p>","DOI":"10.1145\/1059816.1059820","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"16-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":50,"title":["Probabilistic model checking in practice"],"prefix":"10.1145","volume":"32","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"University of Birmingham, Edgbaston, Birmingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"University of Birmingham, Edgbaston, Birmingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[{"name":"University of Birmingham, Edgbaston, Birmingham, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2005,3]]},"reference":[{"key":"e_1_2_1_1_1","unstructured":"PRISM web site. www.cs.bham.ac.uk\/~dxp\/prism.]]  PRISM web site. www.cs.bham.ac.uk\/~dxp\/prism.]]"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2003.1205180"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.012"},{"key":"e_1_2_1_4_1","volume-title":"Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04)","author":"Duflot M.","year":"2004","unstructured":"M. Duflot , M. Kwiatkowska , G. Norman , and D. Parker . A formal analysis of Bluetooth device discovery . In Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04) , 2004 . To appear.]] M. Duflot, M. Kwiatkowska, G. Norman, and D. Parker. A formal analysis of Bluetooth device discovery. In Proc. 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), 2004. To appear.]]"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3812.3818"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.04.004"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TNANO.2002.807393"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(90)90107-9"},{"key":"e_1_2_1_9_1","series-title":"LNCS","first-page":"347","volume-title":"Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00)","author":"Hermanns H.","year":"2000","unstructured":"H. Hermanns , J.-P. Katoen , J. Meyer-Kayser , and M. Siegle . A Markov chain model checker . In S. Graf and M. Schwartzbach, editors, Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00) , volume 1785 of LNCS , pages 347 -- 362 . Springer , 2000 .]] H. Hermanns, J.-P. Katoen, J. Meyer-Kayser, and M. Siegle. A Markov chain model checker. In S. Graf and M. Schwartzbach, editors, Proc. 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'00), volume 1785 of LNCS, pages 347--362. Springer, 2000.]]"},{"key":"e_1_2_1_11_1","series-title":"LNCS","first-page":"194","volume-title":"Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02)","author":"Kwiatkowska M.","year":"2002","unstructured":"M. Kwiatkowska and G. Norman . Verifying randomized Byzantine agreement . In D. Peled and M. Vardi, editors, Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02) , volume 2529 of LNCS , pages 194 -- 209 . Springer , 2002 .]] M. Kwiatkowska and G. Norman. Verifying randomized Byzantine agreement. In D. Peled and M. Vardi, editors, Proc. Formal Techniques for Networked and Distributed Systems (FORTE'02), volume 2529 of LNCS, pages 194--209. Springer, 2002.]]"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1025129.1026103"},{"key":"e_1_2_1_13_1","series-title":"LNCS","first-page":"105","volume-title":"Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03)","author":"Kwiatkowska M.","year":"2003","unstructured":"M. Kwiatkowska , G. Norman , D. Parker , and J. Sproston . Performance analysis of probabilistic timed automata using digital clocks . In K. Larsen and P. Niebert, editors, Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03) , volume 2791 of LNCS , pages 105 -- 120 . Springer-Verlag , 2003 .]] M. Kwiatkowska, G. Norman, D. Parker, and J. Sproston. Performance analysis of probabilistic timed automata using digital clocks. In K. Larsen and P. Niebert, editors, Proc. Formal Modeling and Analysis of Timed Systems (FORMATS'03), volume 2791 of LNCS, pages 105--120. Springer-Verlag, 2003.]]"},{"key":"e_1_2_1_14_1","series-title":"LNCS","first-page":"194","volume-title":"Proc. 13th International Conference on Computer Aided Verification (CAV'01)","author":"Kwiatkowska M.","year":"2001","unstructured":"M. Kwiatkowska , G. Norman , and R. Segala . Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM . In G. Berry, H. Comon, and A. Finkel, editors, Proc. 13th International Conference on Computer Aided Verification (CAV'01) , volume 2102 of LNCS , pages 194 -- 206 . Springer , 2001 .]] M. Kwiatkowska, G. Norman, and R. Segala. Automated verification of a randomized distributed consensus protocol using Cadence SMV and PRISM. In G. Berry, H. Comon, and A. Finkel, editors, Proc. 13th International Conference on Computer Aided Verification (CAV'01), volume 2102 of LNCS, pages 194--206. Springer, 2001.]]"},{"key":"e_1_2_1_15_1","series-title":"LNCS","first-page":"169","volume-title":"Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV'02)","author":"Kwiatkowska M.","year":"2002","unstructured":"M. Kwiatkowska , G. Norman , and J. Sproston . Probabilistic model checking of the IEEE 802.11 wireless local area network protocol . In H. Hermanns and R. Segala, editors, Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV'02) , volume 2399 of LNCS , pages 169 -- 187 . Springer , 2002 .]] M. Kwiatkowska, G. Norman, and J. Sproston. Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In H. Hermanns and R. Segala, editors, Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV'02), volume 2399 of LNCS, pages 169--187. Springer, 2002.]]"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650300007"},{"key":"e_1_2_1_17_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"293","DOI":"10.1007\/978-3-540-30206-3_21","volume-title":"Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT)","author":"Kwiatkowska M.","year":"2004","unstructured":"M. Kwiatkowska , G. Norman , J. Sproston and F. Wang . Symbolic model checking for probabilistic timed automata . In Y. Lakhnech and S. Yovine, editors, Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT) , volume 3253 of LNCS , pages 293 -- 308 . Springer , 2004 .]] M. Kwiatkowska, G. Norman, J. Sproston and F. Wang. Symbolic model checking for probabilistic timed automata. In Y. Lakhnech and S. Yovine, editors, Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant Systems (FTRTFT), volume 3253 of LNCS, pages 293--308. Springer, 2004.]]"},{"key":"e_1_2_1_18_1","volume-title":"Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04)","author":"Lanotte R.","year":"2004","unstructured":"R. Lanotte , A. Maggiolo-Schettini , and A. Troina . Automatic analysis of a non-repudiation protocol . In Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04) , 2004 .]] R. Lanotte, A. Maggiolo-Schettini, and A. Troina. Automatic analysis of a non-repudiation protocol. In Proc. 2nd International Workshop on Quantitative Aspects of Programming Languages (QAPL'04), 2004.]]"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.08.072"},{"key":"e_1_2_1_20_1","unstructured":"A. McIver and C. Morgan. An elementary proof that Herman's ring is &theta;(n2). Submitted for publication.]]  A. McIver and C. Morgan. An elementary proof that Herman's ring is &theta;(n2). Submitted for publication.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2005.852033"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1114283.1114487"},{"key":"e_1_2_1_24_1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"81","DOI":"10.1007\/978-3-540-40981-6_9","volume-title":"Proc. BCS-FACS Formal Aspects of Security (FASec'02)","author":"Norman G.","year":"2003","unstructured":"G. Norman and V. Shmatikov . Analysis of probabilistic contract signing . In A. Abdallah, P. Ryan, and S. Schneider, editors, Proc. BCS-FACS Formal Aspects of Security (FASec'02) , volume 2629 of LNCS , pages 81 -- 96 . Springer , 2003 .]] G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. In A. Abdallah, P. Ryan, and S. Schneider, editors, Proc. BCS-FACS Formal Aspects of Security (FASec'02), volume 2629 of LNCS, pages 81--96. Springer, 2003.]]"},{"key":"e_1_2_1_25_1","volume-title":"Analysis of probabilistic contract signing. Submitted","author":"Norman G.","year":"2005","unstructured":"G. Norman and V. Shmatikov . Analysis of probabilistic contract signing. Submitted , 2005 .]] G. Norman and V. Shmatikov. Analysis of probabilistic contract signing. Submitted, 2005.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/502059.502044"},{"key":"e_1_2_1_27_1","series-title":"CRM Monograph Series","doi-asserted-by":"crossref","DOI":"10.1090\/crmm\/023","volume-title":"Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems","author":"Rutten J.","year":"2004","unstructured":"J. Rutten , M. Kwiatkowska , G. Norman , and D. Parker . Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems , P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series . American Mathematical Society , 2004 .]] J. Rutten, M. Kwiatkowska, G. Norman, and D. Parker. Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, P. Panangaden and F. van Breugel (eds.), volume 23 of CRM Monograph Series. American Mathematical Society, 2004.]]"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1297352.1297359"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1515\/9781400882618-003"}],"container-title":["ACM SIGMETRICS Performance Evaluation Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1059816.1059820","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1059816.1059820","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:31:46Z","timestamp":1750264306000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1059816.1059820"}},"subtitle":["case studies with PRISM"],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":27,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["10.1145\/1059816.1059820"],"URL":"https:\/\/doi.org\/10.1145\/1059816.1059820","relation":{},"ISSN":["0163-5999"],"issn-type":[{"type":"print","value":"0163-5999"}],"subject":[],"published":{"date-parts":[[2005,3]]},"assertion":[{"value":"2005-03-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}