{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:36:21Z","timestamp":1770284181220,"version":"3.49.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2003,4,1]],"date-time":"2003-04-01T00:00:00Z","timestamp":1049155200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2003,4]]},"abstract":"<jats:title>Abstract.<\/jats:title>\n          <jats:p>The interplay of real time and probability is crucial to the correctness of the IEEE 1394 FireWire root contention protocol. We present a formal verification of the protocol using probabilistic model checking. Rather than analyse the functional aspects of the protocol, by asking such questions as \u2018Will a leader be elected?\u2019, we focus on the protocol's performance, by asking the question \u2018How certain are we that a leader will be elected sufficiently quickly?\u2019 Probabilistic timed automata are used to formally model and verify the protocol against properties which require that a leader is elected before a deadline with a certain probability. We use techniques such as abstraction, reachability analysis and integer-time semantics to aid the model-checking process, and the efficacy of these techniques is compared.<\/jats:p>","DOI":"10.1007\/s001650300007","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"295-318","source":"Crossref","is-referenced-by-count":64,"title":["Probabilistic Model Checking of Deadline Properties in the IEEE 1394 FireWire Root Contention Protocol"],"prefix":"10.1145","volume":"14","author":[{"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, UK, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[{"name":"School of Computer Science, University of Birmingham, Birmingham, UK, , , , , , GB"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jeremy","family":"Sproston","sequence":"additional","affiliation":[{"name":"Dipartimento di Informatica, Universit\u00e0 di Torino, Torino, Italy, , , , , , IT"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","series-title":"LNCS","first-page":"115","volume-title":"Proceedings of the 18th International Conference on Automata, Languages and Programming (ICALP'91)","author":"Alur R.","year":"1991"},{"issue":"2","key":"p_2","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","article-title":"A theory of timed automata","volume":"126","author":"Al","year":"1994","journal-title":"Theoretical Computer Science"},{"issue":"1","key":"p_3","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1006\/inco.1995.1059","article-title":"Timing verification by successive approximation","volume":"18","author":"Alur R.","year":"1995","journal-title":"Information and Computation"},{"key":"p_4","first-page":"470","volume-title":"Sangiorgi and de Simone [Sad98]","author":"Asarin E."},{"issue":"3","key":"p_5","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","article-title":"Model checking for a probabilistic branching time logic with fairness","volume":"11","author":"Ba","year":"1998","journal-title":"Distributed Computing"},{"key":"p_6","series-title":"LNCS","first-page":"318","volume-title":"Proceedings of the 10th International Symposium of Formal Methods Europe (FME","author":"Bey","year":"2001"},{"key":"p_7","first-page":"142","volume-title":"Proceedings of the 10th International Conference on Concurrency Theory (CONCUR'99)","volume":"1664","author":"Baier C.","year":"1999"},{"key":"p_8","series-title":"LNCS","first-page":"499","volume-title":"Proceedings of the International Conference on the Foundations of Software Technology and Theoretical Computer Science (FSTTCS'95)","author":"Bid","year":"1995"},{"key":"p_9","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/3-540-48153-2_11","volume-title":"Proceedings of the 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME'99)","author":"Bozga M.","year":"1999"},{"key":"p_10","first-page":"207","volume-title":"Proceedings of the 7th International Conference on Real-Time Computing Systems and Applications (RTCSA 2000","author":"Bandini G.","year":"2000"},{"key":"p_11","series-title":"LNCS","first-page":"52","volume-title":"Proceedings of the Workshop on Logics of Programs","author":"Cl","year":"1981"},{"key":"p_12","first-page":"1","volume-title":"Proceedings of the International Workshop on Logic Synthesis (IWLS'93)","author":"Clarke E. M.","year":"1993"},{"key":"p_13","volume-title":"Proceedings of the Workshop on Real-Time Tools (RT-TOOLS 2001)","author":"Co","year":"2001"},{"key":"p_15","first-page":"423","volume-title":"Sangiorgi and de Simone [Sad98]","author":"de Alfaro L."},{"key":"p_17","series-title":"LNCS","first-page":"395","volume-title":"Proceedings of the 6th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS","author":"de Alfaro L.","year":"2000"},{"key":"p_18","volume-title":"Finite-State Markovian Decision Processes","author":"Der","year":"1970"},{"key":"p_19","series-title":"LNCS","first-page":"39","volume-title":"Proceedings of the Joint PAPM-PROBMIV 2001 Workshop","author":"D'Argenio P. R.","year":"2001"},{"key":"p_20","first-page":"107","volume-title":"Proceedings of the 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2002","author":"Daws C.","year":"2002"},{"key":"p_21","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III: Verification and Control","author":"Daws C.","year":"1996"},{"key":"p_22","first-page":"313","volume-title":"Steffen [Ste98]","author":"Da"},{"key":"p_23","first-page":"66","volume-title":"Proceedings of the 16th IEEE Real-Time Systems Symposium (RTSS'95)","author":"Da","year":"1995"},{"key":"p_24","volume-title":"Proceedings of the International Workshop on Application of Formal Methods to IEEE 1394 Standard","author":"Fi","year":"2001"},{"issue":"5","key":"p_25","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","article-title":"A logic for reasoning about time and reliability","volume":"6","author":"Ha","year":"1994","journal-title":"Formal Aspects of Computing"},{"key":"p_26","series-title":"LNCS","first-page":"41","volume-title":"Proceedings of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'95)","author":"Henzinger T. A.","year":"1995"},{"key":"p_27","volume-title":"HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1(1+2):110-122","author":"Henzinger T. A.","year":"1997"},{"key":"p_28","doi-asserted-by":"crossref","unstructured":"[HMP92] \n      Henzinger T. A. Manna Z.\n     and \n      Pnueli A\n  .: \n  What good are digital clocks? In W\n  . Kuich editor Proceedings of the 19th International Colloquium on Automata Languages and Programming (ICALP'92) volume \n  623\n   of \n  LNCS pages \n  545\n  -\n  558\n  . \n  Springer-Verlag 1992\n  .","DOI":"10.1007\/3-540-55719-9_103"},{"key":"p_29","series-title":"LNCS","first-page":"189","volume-title":"T. Margaria and W. Yi","author":"Hune T. S.","year":"2001"},{"issue":"3","key":"p_30","doi-asserted-by":"crossref","first-page":"356","DOI":"10.1145\/2166.357214","article-title":"Termination of probabilistic concurrent programs","volume":"5","author":"Hart S.","year":"1983","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"p_31","series-title":"LNCS","volume-title":"editor","author":"Kat","year":"1999"},{"key":"p_32","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Proceedings of the 12th International Conference on Computer Performance Evaluation, Modelling Techniques and Tools (TOOLS","author":"Kwiatkowska M. Z.","year":"2002"},{"key":"p_33","first-page":"169","volume-title":"Proceedings of the Joint PAPM-PROBMIV 2002 Workshop","volume":"2399","author":"Kwiatkowska M. Z.","year":"2002"},{"issue":"1","key":"p_34","doi-asserted-by":"crossref","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","article-title":"Automatic verification of real-time systems with discrete probability distributions","volume":"282","author":"Kwiatkowska M. Z.","year":"2002","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"p_35","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","article-title":"Semantics of probabilistic programs","volume":"22","author":"Koz","year":"1981","journal-title":"Journal of Computer and System Sciences"},{"key":"p_36","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"W: Denumerable Markov Chains","author":"Kemeny J. G.","year":"1976","edition":"2"},{"key":"p_37","volume-title":"Uppaal in a nutshell. Software Tools for Technology Transfer, 1(1+2):134-152","author":"Larsen K. G.","year":"1997"},{"key":"p_38","first-page":"281","volume-title":"Steffen [Ste98]","author":"Lindahl M."},{"key":"p_39","unstructured":"[Pri] PRISM: Web page: http : \/\/www.cs.bham.ac.uk\/ \u223c dxp\/prism\/"},{"key":"p_40","series-title":"LNCS","volume-title":"editors","author":"Sad","year":"1998"},{"issue":"2","key":"p_42","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Se","year":"1995","journal-title":"Nordic Journal of Computing"},{"issue":"4","key":"p_43","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1007\/s100090100059","article-title":": Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k","volume":"3","author":"Si","year":"2001","journal-title":"Software Tools for Technology Transfer"},{"key":"p_44","series-title":"LNCS","volume-title":"editor","author":"Ste","year":"1998"},{"key":"p_45","first-page":"53","volume-title":"Katoen [Kat99]","author":"St"},{"key":"p_46","first-page":"327","volume-title":"Proceedings of the 26th IEEE Symposium on Foundations of Computer Science (FOCS'85)","author":"Var","year":"1985"},{"key":"p_47","first-page":"223","volume-title":"Proceedings of the 7th International Conference on Formal Description Techniques (FORTE'94)","author":"Yi W.","year":"1994"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650300007.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650300007\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650300007","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:42:47Z","timestamp":1641483767000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650300007"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,4]]},"references-count":44,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,4]]}},"alternative-id":["10.1007\/s001650300007"],"URL":"https:\/\/doi.org\/10.1007\/s001650300007","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,4]]}}}