{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:27:12Z","timestamp":1761596832277},"reference-count":29,"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 IEEE 1394 Root Contention Protocol is an industrial leader election algorithm for two processes in which probability, real time and parameters play an important role. This protocol has been analysed in various case studies, using a variety of verification and analysis methods. In this paper, we survey and compare several of these case studies.<\/jats:p>","DOI":"10.1007\/s001650300009","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"328-337","source":"Crossref","is-referenced-by-count":18,"title":["Fun with FireWire: A Comparative Study of Formal Verification Methods Applied to the IEEE 1394 Root Contention Protocol"],"prefix":"10.1145","volume":"14","author":[{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"first","affiliation":[{"name":"Department of Computer Engineering, University of California at Santa Cruz, California, USA, , , , , , US"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 13th International Conference on Computer Aided Verification","author":"Annichini A.","year":"2001"},{"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"},{"key":"p_3","first-page":"592","volume-title":"25th Annual ACM Symposium on Theory of Computing (STOC'93)","author":"Alur R.","year":"1993"},{"key":"p_5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60693-9","volume-title":"Proceeding of Foundations of Software Technology and Theoretical Computer Science","author":"Bid","year":"1995"},{"key":"p_6","first-page":"73","volume-title":"Proceedings of the 7th ASCI Conference","author":"Bandini G.","year":"2000"},{"key":"p_7","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_8","volume-title":"Proceedings of the Workshop on Real-Time Tools (RT-TOOLS'2001)","author":"Co","year":"2001"},{"key":"p_10","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"de Alfaro L.","year":"2000"},{"key":"p_11","volume-title":"Proceedings of 7th International Workshop on Formal Methods for Industrial Critical Systems (FMICS'02)","author":"Daws C.","year":"2002"},{"key":"p_12","volume-title":"Proceedings of the International Workshop on Application of Formal Methods to the IEEE1394 Standard Berlin","author":"Fi","year":"2001"},{"key":"p_13","volume-title":"Software Tools for Technology Transfer","volume":"1","author":"Henzinger T. A.","year":"1997"},{"key":"p_14","first-page":"183","volume-title":"Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming","author":"Hune T. S.","year":"2002"},{"key":"p_15","first-page":"200","volume-title":"Computer Performance Evaluation\/TOOLS","author":"Kwiatkowska M. Z.","year":"2002"},{"issue":"3","key":"p_16","doi-asserted-by":"crossref","first-page":"295","DOI":"10.1007\/s001650300007","article-title":"Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. In S. Maharaj, C. Shankland and J. M. T. Romijn, editors","volume":"14","author":"Kwiatkowska M. Z.","year":"2002","journal-title":"Formal Aspects of Computing"},{"key":"p_17","first-page":"101","volume-title":"Automatic verification of real-time systems with discrete probability distributions. Theoretical Computer Science, 268","author":"Kwiatkowska M. Z.","year":"2002"},{"key":"p_18","volume-title":"August","author":"La","year":"1997"},{"key":"p_19","first-page":"314","volume-title":"Proceedings of the 13th Annual ACM Symposium on the Principles of Distributed Computing","author":"Lynch N. A.","year":"1994"},{"key":"p_20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/BFb0055344","volume-title":"Proceedings of the Fifth International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT'98), Lyngby, Denmark","author":"Lutje Spelberg R. F.","year":"1998"},{"key":"p_21","series-title":"Lecture Notes in Computer Science","first-page":"19","volume-title":"J.-P","author":"Mc","year":"1999"},{"key":"p_22","volume-title":": Symbolic Model Checking: An Approach to the State Explosion Problem","author":"Mc","year":"1993"},{"key":"p_23","first-page":"14","article-title":"pGCL: formal reasoning for random algorithms","volume":"22","author":"Mo","year":"1999","journal-title":"South African Computer Journal"},{"issue":"3","key":"p_24","first-page":"200","article-title":"Introduction to the IEEE1394 FireWire","volume":"14","author":"Maharaj S.","year":"2002","journal-title":"Formal Aspects of Computing"},{"key":"p_25","first-page":"1145","article-title":"A survey of formal methods applied to leader election in IEEE 1394","author":"Ma","year":"2000","journal-title":"Journal of Universal Computer Science"},{"key":"p_27","first-page":"143","volume-title":"Proceedings of the Workshop on Formal Methods Computation","author":"Sha","year":"1999"},{"issue":"2","key":"p_28","first-page":"250","article-title":"Probabilistic simulations for probabilistic processes","volume":"2","author":"Se","year":"1995","journal-title":"Nordic Journal of Computing"},{"key":"p_29","volume-title":"Mechanical verification of the IEEE 1394a root contention protocol using Uppaal2k","author":"Si","year":"2001"},{"key":"p_31","first-page":"35","volume-title":"Proceedings of the International Workshop on Application of Formal Methods to the IEEE1394 Standard Berlin","author":"Sto","year":"2001"},{"key":"p_32","first-page":"103","volume-title":"Proceedings of the Workshop on Formal Methods and Telecommunications, (WFMT'99)","author":"Sh","year":"1999"},{"key":"p_33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1142\/4109","volume-title":"J.-P","author":"St","year":"1999"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650300009.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650300009\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650300009","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:43:26Z","timestamp":1641483806000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650300009"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,4]]},"references-count":29,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,4]]}},"alternative-id":["10.1007\/s001650300009"],"URL":"https:\/\/doi.org\/10.1007\/s001650300009","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,4]]}}}