Open access
Date
2008Type
- Report
ETH Bibliography
yes
Altmetrics
Abstract
We present a formal development in Event-B of a distributed topology discovery algorithm. Distributed topology discovery is at the core 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 specify these by appropriately combining invariants, event refinement, and proofs of 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. Show more
Permanent link
https://doi.org/10.3929/ethz-a-006733606Publication status
publishedJournal / series
Technical reportVolume
Publisher
ETH, Department of Computer ScienceSubject
SPECIFICATION LANGUAGES (COMPUTER SYSTEMS); ROUTING (COMPUTER SYSTEMS); PROGRAMS AND ALGORITHMS FOR THE SOLUTION OF SPECIAL PROBLEMS; SPEZIFIKATIONSSPRACHEN (COMPUTERSYSTEME); PROGRAMME UND ALGORITHMEN ZUR LÖSUNG SPEZIELLER PROBLEME; WEGEERMITTLUNG (COMPUTERSYSTEME)Organisational unit
02150 - Dep. Informatik / Dep. of Computer Science
More
Show all metadata
ETH Bibliography
yes
Altmetrics