A mixed approach for the formal correctness proof of distributed programs

The paper presents a mixed approach in the formal correctness proof of distributed programs. Coloured Petri Nets are used to model the system and proof rules derived both from the Petri Net Theory and the Assertional Reasoning Theory are used to carry out the proof of the desired system properties. A correctness proof of a distributed computing system used in a nuclear fusion experiment is then presented in detail, in order to illustrate the applicability of the proposed methodology in real-world distributed systems.