Proving correctness of distributed algorithms using high-level Petri nets-a case study

Author

Desel, Jörg ; Kindler, Ekkart

Author_Institution

Inst. fur Angewandte Inf. und Formale Beschreibungsverfahren, Karlsruhe Univ., Germany

fYear

1998

fDate

23-26 Mar 1998

Firstpage

177

Lastpage

186

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 logic. As a nontrivial case study we present a variant of Raymond´s (1989) message passing mutual exclusion algorithm that works on arbitrary connected networks

Keywords

Petri nets; algebraic specification; distributed algorithms; message passing; program verification; temporal logic; arbitrary connected networks; case study; distributed algorithm correctness proving; high-level Petri nets; message passing algorithms; mutual exclusion algorithm; proof technique; temporal logic style language; Computer aided software engineering; Distributed algorithms; Electronic switching systems; Logic; Petri nets; Read only memory; Safety; Specification languages; System recovery;

fLanguage

English

Publisher

ieee

Conference_Titel

Application of Concurrency to System Design, 1998. Proceedings., 1998 International Conference on

Conference_Location

Fukushima

Print_ISBN

0-8186-8350-3

Type

conf

DOI

10.1109/CSD.1998.657550

Filename

657550