{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T23:17:50Z","timestamp":1756682270060,"version":"3.43.0"},"reference-count":27,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2000,6,1]],"date-time":"2000-06-01T00:00:00Z","timestamp":959817600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2000,6,1]],"date-time":"2000-06-01T00:00:00Z","timestamp":959817600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2000,6]]},"DOI":"10.1023\/a:1008764923992","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"307-320","source":"Crossref","is-referenced-by-count":25,"title":["Verification of a Leader Election Protocol: Formal Methods Applied to IEEE 1394"],"prefix":"10.1007","volume":"16","author":[{"given":"Marco","family":"Devillers","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Griffioen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Judi","family":"Romijn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Frits","family":"Vaandrager","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"260866_CR1","unstructured":"M. Archer and C. Heitmeyer, \u201cMechanical verification of timed automata: A case study, \u201d in Proceedings IEEE Real-Time Technology and Applications Symposium (RTAS'96), IEEE Computer Society Press, 1996."},{"key":"260866_CR2","doi-asserted-by":"crossref","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saidi, \u201cPowerful techniques for the automatic generation of invariants, \u201d in R. Alur and T.A. Henzinger (Eds.), Proceedings of the 8th International Conference on Computer Aided Verification, New Brunswick, NJ, USA. Lecture Notes in Computer Science, Vol. 1102, Springer-Verlag, July\/August 1996, pp. 323\u2013335.","DOI":"10.1007\/3-540-61474-5_80"},{"issue":"2","key":"260866_CR3","doi-asserted-by":"crossref","first-page":"152","DOI":"10.1093\/comjnl\/38.2.152","volume":"38","author":"C.-T. Chou","year":"1995","unstructured":"C.-T. Chou, \u201cMechanical verification of distributed algorithms in higher-order logic, \u201d The Computer Journal, Vol. 38, No. 2, pp. 152\u2013161, 1995.","journal-title":"The Computer Journal"},{"key":"260866_CR4","doi-asserted-by":"crossref","unstructured":"M.C.A. Devillers, W.O.D. Griffioen, and O. M\u00fcller, \u201cPossibly infinite sequences: A comparative case study, \u201d in E.L. Gunter and A. Felty (Eds.), 10th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97). Lecture Notes in Computer Science, Vol. 1275, Springer-Verlag, 1997, pp. 89\u2013104.","DOI":"10.1007\/BFb0028388"},{"key":"260866_CR5","doi-asserted-by":"crossref","unstructured":"J.F. Groote and A. Ponse, \u201cThe syntax and semantics of \u03bcCRL, \u201d in A. Ponse, C. Verhoef, and S.F.M. van Vlijmen (Eds.), '94,Workshops in Computing Series, Springer-Verlag, 1995, pp. 26\u201362.","DOI":"10.1007\/978-1-4471-2120-6_2"},{"key":"260866_CR6","doi-asserted-by":"crossref","unstructured":"W.O.D. Griffioen and F.W. Vaandrager, \u201cNormed simulations, \u201d in A.J. Hu and M.Y. Vardi (Eds.), Proceedings of the 10th International Conference on Computer Aided Verification, Vancouver, BC, Canada. Lecture Notes in Computer Science, Vol. 1427, Springer-Verlag, June\/July 1998, pp. 332\u2013344.","DOI":"10.1007\/BFb0028756"},{"key":"260866_CR7","doi-asserted-by":"crossref","unstructured":"L. Helmink, M.P.A. Sellink, and F.W. Vaandrager, \u201cProof-checking a data link protocol, \u201d in H. Barendregt and T. Nipkow (Eds.), Proceedings International Workshop TYPES'93, Nijmegen, The Netherlands, May 1993. Lecture Notes in Computer Science, Vol. 806, Springer-Verlag, 1994, pp. 127\u2013165.","DOI":"10.1007\/3-540-58085-9_75"},{"key":"260866_CR8","doi-asserted-by":"crossref","first-page":"208","DOI":"10.1007\/BF01211619","volume":"9","author":"W.H. Hesselink","year":"1997","unstructured":"W.H. Hesselink, \u201cA mechanical proof of Segall's PIF algorithm, \u201d Formal Aspects of Computing, Vol. 9, pp. 208\u2013226, 1997.","journal-title":"Formal Aspects of Computing"},{"key":"260866_CR9","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1007\/s001650050035","volume":"11","author":"W.H. Hesselink","year":"1999","unstructured":"W.H. Hesselink, \u201cThe verified incremental design of a distributed spanning tree algorithm\u2013extended abstract, \u201d Formal Aspects of Computing, Vol. 11, pp. 45\u201355, 1999.","journal-title":"Formal Aspects of Computing"},{"key":"260866_CR10","unstructured":"IEEE Computer Society, \u201cIEEE standard for a high performance serial bus, \u201d Std 1394-1995, August 1996."},{"key":"260866_CR11","unstructured":"L. K\u00fchne, J. Hooman, and W.P. de Roever, \u201cTowards mechanical verification of parts of the IEEE P1394 serial bus, \u201d in I. Lovrek (Ed.), Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, Zagreb, 1997, pp. 73\u201385."},{"key":"260866_CR12","unstructured":"L. Lamport, \u201cHow to write a proof, \u201d Research Report 94, Digital Equipment Corporation, Systems Research Center, February 1993."},{"key":"260866_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."},{"issue":"3","key":"260866_CR14","first-page":"219","volume":"2","author":"N.A. Lynch","year":"1989","unstructured":"N.A. Lynch and M.R. Tuttle, \u201cAn introduction to input\/output automata, \u201d CWI Quarterly, Vol. 2, No. 3, pp. 219\u2013246, September 1989.","journal-title":"CWI Quarterly"},{"issue":"2","key":"260866_CR15","doi-asserted-by":"crossref","first-page":"214","DOI":"10.1006\/inco.1995.1134","volume":"121","author":"N.A. Lynch","year":"1995","unstructured":"N.A. Lynch and F.W. Vaandrager, \u201cForward and backward simulations, I: Untimed systems, \u201d Information and Computation, Vol. 121, No. 2, pp. 214\u2013233, September 1995.","journal-title":"Information and Computation"},{"key":"260866_CR16","first-page":"43","volume-title":"Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, Zagreb","author":"S.P. Luttik","year":"1997","unstructured":"S.P. Luttik, \u201cDescription and formal specification of the Link layer of P1394, \u201d in I. Lovrek (Ed.), Proceedings of the 2nd International Workshop on Applied Formal Methods in System Design, Zagreb, 1997, pp. 43\u201356. Also available as Report SEN-R9706, CWI, Amsterdam. See URL http:\/\/www.cwi.nl\/~luttik\/."},{"key":"260866_CR17","doi-asserted-by":"crossref","unstructured":"Z. Manna, A. Browne, H.B. Sipma, and T.E. Uribe, \u201cVisual abstraction for temporal verification, \u201d in Proceedings AMAST'98. Lecture Notes in Computer Science, Springer-Verlag, 1998, pp. 28\u201341.","DOI":"10.1007\/3-540-49253-4_5"},{"key":"260866_CR18","unstructured":"O. Mueller, \u201cA verification environment for I\/O automata based on formalized meta-theory,\u201d PhD Thesis, Technical University of Munich, 1998."},{"key":"260866_CR19","doi-asserted-by":"crossref","unstructured":"O. Mueller and T. Nipkow, \u201cTraces of I\/O-automata in Isabelle\/HOLCF, \u201d in M. Bidoit and M. Dauchet (Eds.), Proceedings TAPSOFT'97: Theory and Practice of Software Development, Lille, France. Lecture Notes in Computer Science, Vol. 1214, Springer-Verlag, April 1997, pp. 580\u2013594.","DOI":"10.1007\/BFb0030627"},{"key":"260866_CR20","doi-asserted-by":"crossref","unstructured":"T. Nipkowand K. Slind, \u201cI\/O automata in Isabelle\/HOL, \u201d in P. Dybjer, B. Nordstr\u00f6m, and J. Smith (Eds.), Types for Proofs and Programs. Lecture Notes in Computer Science, Vol. 996, Springer-Verlag, 1995, pp. 101\u2013119.","DOI":"10.1007\/3-540-60579-7_6"},{"issue":"2","key":"260866_CR21","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke, \u201cFormal verification for fault-tolerant architectures: Prolegomena to the design of PVS, \u201d IEEE Transactions on Software Engineering, Vol. 21, No. 2, pp. 107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"260866_CR22","doi-asserted-by":"crossref","unstructured":"W.P. de Roever and K. Engelhardt, Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, 1998. Cambridge Tracts in Theoretical Computer Science, Vol. 47.","DOI":"10.1017\/CBO9780511663079"},{"key":"260866_CR23","unstructured":"J.M.T. Romijn, \u201cA timed verification of the IEEE 1394 leader election protocol, \u201d in S. Gnesi and D. Latella (Eds.), Proceedings of the Fourth International ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS'99), 1999, pp. 3\u201329. Full version available from URL http:www.cs.kun.nl\/~judi."},{"key":"260866_CR24","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/s001650050030","volume":"10","author":"C. Shankland","year":"1998","unstructured":"C. Shankland and M.B. van der Zwaag, \u201cThe tree identify protocol of IEEE 1394 in \u03bcCRL, \u201d Formal Aspects of Computing, Vol. 10, pp. 509\u2013531, 1998.","journal-title":"Formal Aspects of Computing"},{"issue":"1","key":"260866_CR25","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/s100090050018","volume":"2","author":"M. Sighireanu","year":"1998","unstructured":"M. Sighireanu and R. Mateescu, \u201cVerification of the link layer protocol of the IEEE-1394 serial bus (FireWire): an experiment with E-LOTOS, \u201d Springer International Journal on Software Tools for Technology Transfer (STTT), Vol. 2, No. 1, pp. 68\u201388, December 1998.","journal-title":"Springer International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"260866_CR26","doi-asserted-by":"crossref","unstructured":"M.I.A. Stoelinga and F.W. Vaandrager, \u201cRoot contention in IEEE 1394, \u201d in J.-P. Katoen (Ed.), Proceedings 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems, Bamberg, Germany. Lecture Notes in Computer Science, Vol. 1601, Springer-Verlag, 1999, pp. 53\u201374.","DOI":"10.1007\/3-540-48778-6_4"},{"key":"260866_CR27","unstructured":"T.E.J. Vos, \u201cUNITY in diversity: A stratified approach to the verification of distributed algorithms, \u201d Ph.D. Thesis, Utrecht University, January 2000."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008764923992.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008764923992\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008764923992.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T04:22:34Z","timestamp":1754367754000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008764923992"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,6]]},"references-count":27,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,6]]}},"alternative-id":["260866"],"URL":"https:\/\/doi.org\/10.1023\/a:1008764923992","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2000,6]]}}}