DocumentCode
1565824
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
fYear
1988
Firstpage
237
Lastpage
244
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;
fLanguage
English
Publisher
ieee
Conference_Titel
Distributed Computing Systems in the 1990s, 1988. Proceedings., Workshop on the Future Trends of
Print_ISBN
0-8186-0897-8
Type
conf
DOI
10.1109/FTDCS.1988.26703
Filename
26703
Link To Document