--- abstract: 'We present a formal development in Event-B of a distributed topology discovery algorithm. Distributed topology discovery is at the core of several routing algorithms and is the problem of each node in a network discovering and maintaining information on the network topology. One of the key challenges in developing this algorithm is specifying the problem itself. We provide a specification that includes both safety properties, formalizing invariants that should hold in all system states, and liveness properties that characterize when the system reaches stable states. We prove these properties by appropriately combining proofs of invariants, event refinement, event convergence, and deadlock freedom. The combination of these features is novel and should be useful for formalizing and developing other kinds of semi-reactive systems, which are systems that react to, but do not modify, their environment. Our entire development has been formalized and machine checked using the Rodin tool.' accompaniment: [] book_title: ~ commentary: ~ completion_time: ~ composition_type: ~ conductors_id: [] conductors_name: [] contact_email: ~ copyright_holders: [] corp_creators: [] creators_id: - htson@inf.ethz.ch - ~ - basin@inf.ethz.ch - jabrial@inf.ethz.ch creators_name: - family: Hoang given: Thai Son honourific: '' lineage: '' - family: Kuruma given: Hironobu honourific: '' lineage: '' - family: Basin given: David honourific: '' lineage: '' - family: Abrial given: Jean-Raymond honourific: '' lineage: '' data_type: ~ date: 2009-11 date_type: published datestamp: 2010-02-05 09:55:00 department: ~ dir: disk0/00/00/02/03 divisions: [] edit_lock_since: ~ edit_lock_until: ~ edit_lock_user: ~ editors_id: [] editors_name: [] eprint_status: archive eprintid: 203 event_dates: ~ event_location: ~ event_title: ~ event_type: ~ exhibitors_id: [] exhibitors_name: [] fileinfo: '' full_text_status: none funders: [] id_number: ~ importid: ~ institution: ~ isbn: ~ ispublished: pub issn: ~ item_issues_comment: [] item_issues_count: 0 item_issues_description: [] item_issues_id: [] item_issues_reported_by: [] item_issues_resolved_by: [] item_issues_status: [] item_issues_timestamp: [] item_issues_type: [] keywords: ~ lastmod: 2010-02-05 09:55:00 latitude: ~ learning_level: ~ longitude: ~ lyricists_id: [] lyricists_name: [] metadata_visibility: show monograph_type: ~ note: ~ num_pieces: ~ number: 11-12 official_url: http://dx.doi.org/10.1016/j.scico.2009.07.006 output_media: ~ pagerange: 879-899 pages: ~ patent_applicant: ~ pedagogic_type: ~ place_of_pub: ~ pres_type: ~ producers_id: [] producers_name: [] projects: [] publication: Science of Computer Programming publisher: Elsevier refereed: TRUE referencetext: ~ related_url_type: [] related_url_url: [] relation_type: [] relation_uri: [] rev_number: 5 series: ~ skill_areas: [] source: ~ status_changed: 2010-02-05 09:55:00 subjects: - examples succeeds: ~ suggestions: ~ sword_depositor: ~ sword_slug: ~ task_purpose: ~ thesis_type: ~ title: Developing topology discovery in Event-B type: article userid: 16 volume: 74