We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Specification and Verification of the ATMR Protocol Using UNITY: Part 2: Correctness Proof.
- Authors
Charpentier, Michel; Padiou, Gérard
- Abstract
We propose a description and validation of the ATMR protocol within the UNITY formalism. This formal description helps us understand precisely the mechanisms this protocol involves. In particular, we have noted the use of an incorrect detection algorithm to generate reset slots. An operational description using the UNITY programming notation and a specification of the main correctness properties in the UNITY temporal logic are given in a previous part [2]. This second part is dedicated to a hand-made correctness proof. The proof shows that the model satisfies the specification despite the spurious detection in the reset generation mechanism.
- Publication
Parallel Processing Letters, 1998, Vol 8, Issue 4, p433
- ISSN
0129-6264
- Publication type
Article
- DOI
10.1142/S0129626498000444