creators_name: Hoang, Thai Son
creators_name: Kuruma, Hironobu
creators_name: Basin, David
creators_name: Abrial, Jean-Raymond
creators_id: htson@inf.ethz.ch
creators_id: basin@inf.ethz.ch
creators_id: jabrial@inf.ethz.ch
type: article
datestamp: 2010-02-05 10:35:54
lastmod: 2010-02-05 10:35:54
metadata_visibility: show
title: Developing Topology Discovery in Event-B
ispublished: pub
subjects: examples
full_text_status: none
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 is specifying the problem itself. Our specification 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 establish these by appropriately combining proofs of invariant preservation, 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.
date: 2009-02
date_type: published
publication: Integrated Formal Methods
publisher: Springer
pagerange: 1-19
refereed: FALSE
official_url: http://dx.doi.org/10.1007/978-3-642-00255-7_1
citation:   Hoang, Thai Son and Kuruma, Hironobu and Basin, David and Abrial, Jean-Raymond  (2009) Developing Topology Discovery in Event-B.  Integrated Formal Methods .   pp. 1-19.