{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T22:11:16Z","timestamp":1780611076165,"version":"3.54.1"},"reference-count":37,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2011,4,1]],"date-time":"2011-04-01T00:00:00Z","timestamp":1301616000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["214755"],"award-info":[{"award-number":["214755"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004965","name":"Sixth Framework Programme","doi-asserted-by":"publisher","award":["IST-2001-35304"],"award-info":[{"award-number":["IST-2001-35304"]}],"id":[{"id":"10.13039\/501100004965","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61073022"],"award-info":[{"award-number":["61073022"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003246","name":"Nederlandse Organisatie voor Wetenschappelijk Onderzoek","doi-asserted-by":"publisher","award":["612.000.103"],"award-info":[{"award-number":["612.000.103"]}],"id":[{"id":"10.13039\/501100003246","id-type":"DOI","asserted-by":"publisher"}]},{"name":"PROGRESS","award":["TES4199"],"award-info":[{"award-number":["TES4199"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2011,4]]},"abstract":"<jats:p>The model checker Uppaal is used to formally model and analyze parts of Zeroconf, a protocol for dynamic configuration of IPv4 link-local addresses that has been defined in RFC 3927 of the IETF. Our goal has been to construct a model that (a) is easy to understand by engineers, (b) comes as close as possible to the informal text (for each transition in the model there should be a corresponding piece of text in the RFC), and (c) may serve as a basis for formal verification. Our modeling efforts revealed several errors (or at least ambiguities) in the RFC that no one else spotted before. We present two proofs of the mutual exclusion property for Zeroconf (for an arbitrary number of hosts and IP addresses): a manual, operational proof, and a proof that combines model checking with the application of a new abstraction relation that is compositional with respect to committed locations. The model checking problem has been solved using Uppaal and the abstractions have been checked by hand.<\/jats:p>","DOI":"10.1145\/1952522.1952527","type":"journal-article","created":{"date-parts":[[2011,5,3]],"date-time":"2011-05-03T12:48:53Z","timestamp":1304426933000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Formal specification and analysis of zeroconf using uppaalS"],"prefix":"10.1145","volume":"10","author":[{"given":"Jasper","family":"Berendsen","sequence":"first","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Biniam","family":"Gebremichael","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Frits W.","family":"Vaandrager","sequence":"additional","affiliation":[{"name":"Radboud University Nijmegen, The Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Miaomiao","family":"Zhang","sequence":"additional","affiliation":[{"name":"Tongji University, Shanghai, China"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2011,5,5]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186058"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_2_1_3_1","unstructured":"Bauer J. 2006. Analysis of communication topologies by partner abstraction. Ph.D. dissertation. Universit&amp;#228;t des Saarlandes Saarbr&amp;#252;cken Germany.  Bauer J. 2006. Analysis of communication topologies by partner abstraction. Ph.D. dissertation. Universit&amp;#228;t des Saarlandes Saarbr&amp;#252;cken Germany."},{"key":"e_1_2_1_4_1","doi-asserted-by":"crossref","unstructured":"Behrmann G. David A. and \n      \n      \n      Larsen K\n      \n  \n  . \n  2004\n  . A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems International School on Formal Methods for the Design of Computer Communication and Software Systems Revised Lectures M. Bernardo and F. Corradini Eds. Lecture Notes in Computer Science vol. \n  3185\n  . \n  Springer Berlin Germany 200--236.  Behrmann G. David A. and Larsen K. 2004. A tutorial on Uppaal. In Formal Methods for the Design of Real-Time Systems International School on Formal Methods for the Design of Computer Communication and Software Systems Revised Lectures M. Bernardo and F. Corradini Eds. Lecture Notes in Computer Science vol. 3185. Springer Berlin Germany 200--236.","DOI":"10.1007\/978-3-540-30080-9_7"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85778-5_17"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(92)90005-V"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the International Conference on Dependable Systems and Networks. IEEE Computer Society","author":"Bohnenkamp H."},{"key":"e_1_2_1_9_1","unstructured":"Brinksma E. and Mader A. 2004. On verification modelling of embedded systems. Tech. rep. TR-CTIT-04-03. Centre for Telematics and Information Technology University of Twente Twente The Netherlands.  Brinksma E. and Mader A. 2004. On verification modelling of embedded systems. Tech. rep. TR-CTIT-04-03. Centre for Telematics and Information Technology University of Twente Twente The Netherlands."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the International Symposium on Software Engineering for Parallel and Distributed Systems. IEEE Computer Society Press, 198--205","author":"Bruns G."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_9"},{"key":"e_1_2_1_12_1","unstructured":"Cheshire S. 2006. Personal communication.  Cheshire S. 2006. Personal communication."},{"key":"e_1_2_1_13_1","doi-asserted-by":"crossref","unstructured":"Cheshire S. Aboba B. and Guttman E. 2005. Dynamic configuration of IPv4 link-local addresses (RFC 3927). http:\/\/www.ietf.org\/rfc\/rfc3927.txt.  Cheshire S. Aboba B. and Guttman E. 2005. Dynamic configuration of IPv4 link-local addresses (RFC 3927). http:\/\/www.ietf.org\/rfc\/rfc3927.txt.","DOI":"10.17487\/rfc3927"},{"key":"e_1_2_1_14_1","unstructured":"Cheshire S. and Steinberg D. 2005. Zero Configuration Networking: The Definite Guide. O'Reilly Media Inc. San Francisco CA.   Cheshire S. and Steinberg D. 2005. Zero Configuration Networking: The Definite Guide. O'Reilly Media Inc. San Francisco CA."},{"key":"e_1_2_1_15_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the Workshop on Tools and Algorithmes for the Construction and Analysis of Systems","author":"Chkliaev D."},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of the International Conference on Computer Hardware Description Languages and there Application. 15--30","author":"Clarke E. M."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008764923992"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2005.42"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1176887.1176923"},{"key":"e_1_2_1_20_1","volume-title":"Proceedings of the 1st International Workshop on Formal Modeling and Analysis of Timed Systems. Lecture Notes in Computer Science","volume":"2791","author":"Hendriks M."},{"key":"e_1_2_1_21_1","unstructured":"Hoare C. 1985. Communicating Sequential Processes. Prentice-Hall International Englewood Cliffs NJ.   Hoare C. 1985. Communicating Sequential Processes. Prentice-Hall International Englewood Cliffs NJ."},{"key":"e_1_2_1_22_1","unstructured":"Holzmann G. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison Wesley Readings MA.   Holzmann G. 2004. The SPIN Model Checker: Primer and Reference Manual. Addison Wesley Readings MA."},{"key":"e_1_2_1_23_1","volume-title":"Proceedings of the 11th IFIP WG10.2 International Conference on Computer Hardware Description Languages and their Applications, D. Agnew, L. J. M. Claesen, and R. Camposano, Eds., IFIP Transactions","volume":"32","author":"Ip C."},{"key":"e_1_2_1_24_1","doi-asserted-by":"crossref","unstructured":"Jensen H. Larsen K. and \n      \n      \n      Skou A\n      \n  \n  . \n  2000\n  . Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In Proceedings of the 6th Annual Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems M. Joseph Ed. Lecture Notes in Computer Science vol. \n  1926\n  . \n  Springer Berlin Germany 19--30.   Jensen H. Larsen K. and Skou A. 2000. Scaling up Uppaal: Automatic verification of real-time systems using compositionality and abstraction. In Proceedings of the 6th Annual Symposium Formal Techniques in Real-Time and Fault-Tolerant Systems M. Joseph Ed. Lecture Notes in Computer Science vol. 1926. Springer Berlin Germany 19--30.","DOI":"10.1007\/3-540-45352-0_4"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the 1st International Conference on Quantitative Evaluation of Systems. IEEE Computer Society Press","author":"Kwiatkowska M."},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"Kwiatkowska M. Norman G. Parker D. and \n      \n      \n      Sproston J\n      \n  \n  . \n  2003\n  . Performance analysis of probabilistic timed automata using digital clocks. In Proceedings of the Conference on Formal Modeling and Analysis of Timed Systems K. Larsen and P. Niebert Eds. Lecture Notes in Computer Science vol. \n  2791\n  . \n  Springer-Verlag Berlin Germany 105--120.  Kwiatkowska M. Norman G. Parker D. and Sproston J. 2003. Performance analysis of probabilistic timed automata using digital clocks. In Proceedings of the Conference on Formal Modeling and Analysis of Timed Systems K. Larsen and P. Niebert Eds. Lecture Notes in Computer Science vol. 2791. Springer-Verlag Berlin Germany 105--120.","DOI":"10.1007\/978-3-540-40903-8_9"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the 8<sup>th<\/sup> International Workshop on Formal Methods for Parallel Programming: Theory and Applications. IEEE Computer Society Press","author":"Langevelde I. V."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/1086228.1086283"},{"key":"e_1_2_1_29_1","unstructured":"Lynch N. 1996. Distributed Algorithms. Morgan Kaufmann San Fransisco CA.   Lynch N. 1996. Distributed Algorithms. Morgan Kaufmann San Fransisco CA."},{"key":"e_1_2_1_30_1","unstructured":"Milner R. 1989. Communication and Concurrency. Prentice-Hall International Englewood Cliffs NJ.   Milner R. 1989. Communication and Concurrency. Prentice-Hall International Englewood Cliffs NJ."},{"key":"e_1_2_1_31_1","unstructured":"Plummer D. 1982. An Ethernet address resolution protocol (RFC 826). http:\/\/www.ietf.org\/rfc\/rfc826.txt.  Plummer D. 1982. An Ethernet address resolution protocol (RFC 826). http:\/\/www.ietf.org\/rfc\/rfc826.txt."},{"key":"e_1_2_1_32_1","unstructured":"Romijn J. 2004. Improving the quality of protocol standards: Correcting IEEE 1394.1 FireWire net update. Nieuwsbrief Nederland. Verenig. Theoret. Informatica 8 23--30. http:\/\/www.win.tue.nl\/oas\/index.html?iqps\/.  Romijn J. 2004. Improving the quality of protocol standards: Correcting IEEE 1394.1 FireWire net update. Nieuwsbrief Nederland. Verenig. Theoret. Informatica 8 23--30. http:\/\/www.win.tue.nl\/oas\/index.html?iqps\/."},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the 11th International Conference on Computer Aided Verification, N. Halbwachs and D. Peled, Eds., Lecture Notes in Computer Science","volume":"1633","author":"Sifakis J.","year":"1999"},{"key":"e_1_2_1_34_1","volume-title":"Proceedings of the Annual Symposium on Theoretical Aspects of Computer Science, C. Puech and R. Reischuk, Eds. Lecture Notes in Computer Science","volume":"1046","author":"Sifakis J."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650300009"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0008-1"},{"key":"e_1_2_1_37_1","unstructured":"Yorav K. 2000. Exploiting syntactic structure for automatic verification. Ph.D. dissertation The Technion Israel Insitute of Technology Haifa Israel.  Yorav K. 2000. Exploiting syntactic structure for automatic verification. Ph.D. dissertation The Technion Israel Insitute of Technology Haifa Israel."}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1952522.1952527","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1952522.1952527","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T11:39:55Z","timestamp":1750246795000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1952522.1952527"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4]]},"references-count":37,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2011,4]]}},"alternative-id":["10.1145\/1952522.1952527"],"URL":"https:\/\/doi.org\/10.1145\/1952522.1952527","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"value":"1539-9087","type":"print"},{"value":"1558-3465","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4]]},"assertion":[{"value":"2009-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2009-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-05-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}