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.
A mixed approach for the formal correctness proof of distributed programs
G Manduchi
1996
Abstract
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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
