{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,29]],"date-time":"2025-11-29T07:46:29Z","timestamp":1764402389008},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540660101"},{"type":"electronic","value":"9783540487784"}],"license":[{"start":{"date-parts":[[1999,1,1]],"date-time":"1999-01-01T00:00:00Z","timestamp":915148800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48778-6_4","type":"book-chapter","created":{"date-parts":[[2007,5,1]],"date-time":"2007-05-01T06:18:07Z","timestamp":1178000287000},"page":"53-74","source":"Crossref","is-referenced-by-count":36,"title":["Root Contention in IEEE 1394"],"prefix":"10.1007","author":[{"given":"Mari\u00eblle","family":"Stoelinga","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,4,30]]},"reference":[{"issue":"2","key":"4_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"4_CR2","series-title":"Lect Notes Comput Sci","volume-title":"Hybrid Systems III","year":"1996","unstructured":"R. Alur, T.A. Henzinger, and E.D. Sontag, editors. Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996."},{"key":"4_CR3","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/BFb0020949","volume-title":"Hybrid Systems III","author":"J. Bengtsson","year":"1996","unstructured":"J. Bengtsson, K.G. Larsen, F. Larsson, P. Pettersson, and Wang Yi. UPPAAL: a tool suite for the automatic verification of real-time systems. In T.A. Henzinger, and E.D. Sontag, editors. Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996 Alur et al. [2]}, pages 232\u2013243."},{"key":"4_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"208","DOI":"10.1007\/BFb0020947","volume-title":"Hybrid Systems III","author":"C. Daws","year":"1996","unstructured":"C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In T.A. Henzinger, and E.D. Sontag, editors. Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science. Springer-Verlag, 1996 Alur et al. [2]}, pages 208\u2013219."},{"key":"4_CR5","unstructured":"M.C.A. Devillers, W.O.D. Griffioen, J.M.T Romijn, and F.W. Vaandrager. Verification of a leader election protocol \u2014 formal methods applied to IEEE 1394. Technical Report CSI-R9728, Computing Science Institute, University of Nijmegen, December 1997. Submitted."},{"key":"4_CR6","unstructured":"S.J. Garland, N.A. Lynch, and M. Vaziri. IOA: A language for specifiying, programming, and validating distributed systems, September 1997. Available through URL http:\/\/larch.lcs.mit.edu:8001\/~garland\/ioaLanguage.html ."},{"key":"4_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1007\/BFb0028756","volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification","author":"W.O.D. Griffioen","year":"1998","unstructured":"W.O.D. Griffioen and F.W. Vaandrager. Normed simulations. In A.J. Hu and M.Y. Vardi, editors, Proceedings of the 8th International Conference on Computer Aided Verification, Vancouver, BC, Canada, volume 1427 of Lecture Notes in Computer Science, pages 332\u2013344. Springer-Verlag, June\/July 1998."},{"key":"4_CR8","unstructured":"T.A. Henzinger and P.-H. Ho. HyTech: The Cornell HYbrid TECHnology Tool. In U.H. Engberg, K.G. Larsen, and A. Skou, editors, Proceedings of the Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, Denmark, volume NS?95-2 of BRICS Notes Series, pages 29\u201343. Department of Computer Science, University of Aarhus, May 1995."},{"key":"4_CR9","unstructured":"IEEE Computer Society. IEEE Standard for a High Performance Serial Bus. Std 1394-1995, August 1996."},{"key":"4_CR10","unstructured":"IEEE Computer Society. P1394a Draft Standard for a High Performance Serial Bus (Supplement). Draft 2.0, March 1998."},{"key":"4_CR11","unstructured":"L. K\u00fchne, J. Hooman, and W.P. de Roever. Towards mechanical verification of parts of the IEEE P1394 serial bus. In I. Lovrek, editor, Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, Zagreb, pages 73\u201385, 1997."},{"key":"4_CR12","unstructured":"S.P. Luttik. Description and formal specification of the Link layer of P1394. In I. Lovrek, editor, Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, Zagreb, pages 43\u201356, 1997. Also available as Report SEN-R9706, CWI, Amsterdam. See URL http:\/\/www.cwi.nl\/~luttik\/ ."},{"key":"4_CR13","volume-title":"Distributed Algorithms","author":"N.A. Lynch","year":"1996","unstructured":"N.A. Lynch. Distributed Algorithms. Morgan Kaufmann Publishers, Inc., San Fransisco, California, 1996."},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"N.A. Lynch, I. Saias, and R. Segala. Proving time bounds for randomized distributed algorithms. In Proceedings of the 13th Annual ACM Symposium on the Principles of Distributed Computing, pages 314\u2013323, Los Angeles, CA, August 1994.","DOI":"10.1145\/197917.198117"},{"issue":"1","key":"4_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1996.0060","volume":"128","author":"N.A. Lynch","year":"1996","unstructured":"N.A. Lynch and F.W. Vaandrager. Forward and backward simulations, II: Timing-based systems. Information and Computation, 128(1):1\u201325, July 1996.","journal-title":"Information and Computation"},{"key":"4_CR16","unstructured":"MindShare, Inc, and D. Anderson. FireWire System Architecture: IEEE 1394. Addison Wesley, 1998."},{"key":"4_CR17","series-title":"Lect Notes Comput Sci","first-page":"111","volume-title":"Proceedings of 11th International Workshop on Distributed Algorithms (WDAG\u201997)","author":"A. Pogosyants","year":"1997","unstructured":"A. Pogosyants, R. Segala, and N.A. Lynch. Verification of the randomized consensus algorithm of Aspnes and Herlihy: a case study. In M. Mavronicolas and Ph. Tsigas, editors, Proceedings of 11th International Workshop on Distributed Algorithms (WDAG\u201997), Saarbrucken, Germany, September 1997, volume 1320 of Lecture Notes in Computer Science, pages 111\u2013125. Springer-Verlag, 1997. Also, Technical Memo MIT\/LCS\/TM-555, Laboratory for Computer Science, Massachusetts Institute of Technology."},{"key":"4_CR18","series-title":"Available as Technical Report","volume-title":"Modeling and Verification of Randomized Distributed Real-Time Systems","author":"R. Segala","year":"1995","unstructured":"R. Segala. Modeling and Verification of Randomized Distributed Real-Time Systems. PhD thesis, Department of Electrical Engineering and Computer Science, Massachusetts Institute of Technology, June 1995. Available as Technical Report MIT\/LCS\/TR-676."},{"issue":"2","key":"4_CR19","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1006\/inco.1997.2671","volume":"141","author":"R. Segala","year":"1998","unstructured":"R. Segala, R. Gawlick, J.F. S\u00f8gaard-Andersen, and N.A. Lynch. Liveness in timed and untimed systems. Information and Computation, 141(2):119\u2013171, March 1998.","journal-title":"Information and Computation"},{"issue":"2","key":"4_CR20","first-page":"250","volume":"2","author":"R. Segala","year":"1995","unstructured":"R. Segala and N.A. Lynch. Probabilistic simulations for probabilistic processes. Nordic Journal of Computing, 2(2):250\u2013273, 1995.","journal-title":"Nordic Journal of Computing"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"M.I.A. Stoelinga. Gambling for leadership: Root contention in IEEE 1394. Technical Report CSI-R9904, Computing Science Institute, University of Nijmegen, 1999.","DOI":"10.1007\/3-540-48778-6_4"},{"key":"4_CR22","unstructured":"M.I.A. Stoelinga and F.W. Vaandrager. Gambling together in Monte Carlo: Step refinements for probabilistic automata. Technical Report CSI-R99xx, Computing Science Institute, University of Nijmegen, 1999. To appear."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Real-Time and Probabilistic Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-48778-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,27]],"date-time":"2019-04-27T12:35:06Z","timestamp":1556368506000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48778-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540660101","9783540487784"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48778-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}