The Community for Technology Leaders
Proceedings 1998 International Conference on Application of Concurrency to System Design (1998)
Fukushima, Japan
Mar. 23, 1998 to Mar. 26, 1998
ISBN: 0-8186-8350-3
pp: 177
Jörg Desel , Universit?t Karlsruhe
Ekkart Kindler , Humboldt-Universit?t zu Berlin
ABSTRACT
We argue that high-level Petri nets are well suited for the representation of distributed algorithms as well as for correctness proofs. To this end, we provide a simple definition of high-level Petri nets, a way to formulate message-passing algorithms in this notion, a temporal-logic style language for the formulation of properties, and a proof technique which combines techniques from Petri net theory and from temporal logics. As a nontrivial case study, we present a variant of Raymond's message-passing mutual exclusion algorithm that works on arbitrary connected networks.
INDEX TERMS
Distributed algorithms; temporal logic; Petri nets; verification
CITATION

E. Kindler and J. Desel, "Proving Correctness of Distributed Algorithms Using High-Level Petri Nets - A Case Study," Proceedings 1998 International Conference on Application of Concurrency to System Design(ACSD), Fukushima, Japan, 1998, pp. 177.
doi:10.1109/CSD.1998.657550
95 ms
(Ver 3.3 (11022016))