Verification of Fault Tolerant Algorithms Using PEP
Petri net theory is an accepted approach to modelling and verifying distributed algorithms. In this paper we show how a tool based on Petri net theory, the PEP tool, can be used to model and verify fault tolerant algorithms for distributed systems. We conduct three case studies to illustrate our approach and to show the more specific problems we ran into, such as synchronization and crash detection in asynchronous systems, and we explain how we tried to solve them.
Verification; Fault-tolerant algorithms; Petri Nets; Model Checking