Proceedings 1998 International Conference on Application of Concurrency to System Design (1998)
Mar. 23, 1998 to Mar. 26, 1998
Jörg Desel , Universit?t Karlsruhe
Ekkart Kindler , Humboldt-Universit?t zu Berlin
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.
Distributed algorithms; temporal logic; Petri nets; verification
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.