Title :
A characterization of the dynamical ascending routing
Author :
Bouabdallah, A. ; Trehel, M.
Author_Institution :
Lab. d´´Inf. de Besancon, Univ. de Franche-Comte, France
Abstract :
A characterization of a routing defined on a dynamical logical structure is presented. By uniting the structure with the messages destabilizing it, an invariant is obtained, that allows a simple proof of the properties of the routing. The results are exploited by designing and structuring the proof of the mutual exclusion algorithm, which uses this routing. The specifications are done in an axiomatic manner, and the proof is given in a temporal framework
Keywords :
distributed processing; operating systems (computers); programming theory; dynamical ascending routing; dynamical logical structure; mutual exclusion algorithm; proof; specifications; temporal framework; Algorithm design and analysis; Computer networks; Distributed algorithms; Formal specifications; Graph theory; Logic; Nominations and elections; Processor scheduling; Routing; Safety;
Conference_Titel :
Distributed Computing Systems in the 1990s, 1988. Proceedings., Workshop on the Future Trends of
Print_ISBN :
0-8186-0897-8
DOI :
10.1109/FTDCS.1988.26703
