{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T15:39:41Z","timestamp":1725464381724},"reference-count":10,"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>\n            The IEEE 1394 tree identify protocol illustrates the adequacy of the\n            <jats:italic>event-driven approach<\/jats:italic>\n            used together with the B Method. This approach provides a complete framework for developing mathematical models of distributed algorithms. A specific development is made of a series of more and more refined models. Each model is made of a number of static properties (the invariant) and dynamic parts (the guarded events). The internal consistency of each model as well as its correctness with regard to its previous abstraction are proved with the proof engine of Atelier B, which is the tool associated with B. In the case of IEEE 1394 tree identify protocol, the initial model is very primitive: it provides the basic properties of the graph (symmetry, acyclicity, connectivity), and its dynamic parts essentially contain a single event which\n            <jats:italic>elects the leader<\/jats:italic>\n            in one shot. Further refinements introduce more events, showing how each node of the graph non-deterministically participates in the leader election. At some stage in the development, message passing is introduced. This raises a specific potential contention problem, whose solution is given. The last stage of the refinement completely localises the events by making them take decisions based on local data only.\n          <\/jats:p>","DOI":"10.1007\/s001650300002","type":"journal-article","created":{"date-parts":[[2003,12,10]],"date-time":"2003-12-10T21:38:13Z","timestamp":1071092293000},"page":"215-227","source":"Crossref","is-referenced-by-count":57,"title":["A Mechanically Proved and Incremental Development of IEEE 1394 Tree Identify Protocol"],"prefix":"10.1145","volume":"14","author":[{"given":"Jean-Raymond","family":"Abrial","sequence":"first","affiliation":[{"name":"Marseille, France, , , , , , FR"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"Cansell","sequence":"additional","affiliation":[{"name":"Universit\u00e9 de Metz, LORIA, Metz, France, , , , , , FR"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dominique","family":"M\u00e9ry","sequence":"additional","affiliation":[{"name":"Universit\u00e9 Henri Poincar\u00e9 Nancy 1, LORIA, Vand\u0153uvre-l\u00e8s-Nancy, France, , , , , , FR"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"p_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511624162","volume-title":"The B book: Assigning Programs to Meanings","author":"Abrial J.-R.","year":"1996"},{"key":"p_2","first-page":"169","volume-title":"First Conference on the B Method","author":"Abrial J.-R.","year":"1996"},{"key":"p_3","series-title":"Lecture Notes in Computer Science","volume-title":"Introducing dynamic constraints in B","author":"Abrial J.-R.","year":"1998"},{"issue":"1","key":"p_4","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1016\/0022-0000(81)90005-2","article-title":"On correct refinement of programs","volume":"23","author":"Back R. J. R.","year":"1979","journal-title":"Journal of Computer and System Sciences"},{"key":"p_5","volume-title":"Parallel Program Design: A Foundation","author":"Chandy K. M.","year":"1988"},{"key":"p_6","first-page":"3","author":"ClearSy Atelier B","year":"2001","journal-title":"Manuel Utilisateur"},{"key":"p_7","volume-title":": A Discipline of Programming","author":"Dijkstra E. W.","year":"1976"},{"key":"p_8","doi-asserted-by":"crossref","first-page":"307","DOI":"10.1023\/A:1008764923992","article-title":"Verification of a leader election protocol: formal methods applied to IEEE 1394","volume":"16","author":"Devillers M.","year":"2000","journal-title":"Formal Methods in System Design"},{"key":"p_9","volume-title":"IEEE Standard for a High Performance Serial Bus. Std","author":"IEEE.","year":"1995"},{"key":"p_10","first-page":"501","volume-title":"Distributed Algorithms. Morgan Kaufmann","author":"Lynch N.","year":"1996"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s001650300002.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s001650300002\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s001650300002","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:40:04Z","timestamp":1641483604000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s001650300002"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,4]]},"references-count":10,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2003,4]]}},"alternative-id":["10.1007\/s001650300002"],"URL":"https:\/\/doi.org\/10.1007\/s001650300002","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2003,4]]}}}