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 1: Modeling and Specification of the Protocal.
- 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. In this first part, we provide an operational description using the UNITY programming notation as well as a specification of the main correctness properties in the UNITY temporal logic. A second part [2] is dedicated to a hand-made correctness proof. The proof shows that the model satisfies the specification despite this spurious detection. In this study, we apply a general development process based upon the UNITY formalism. During this process, we tune the program specification in order to make the later validation step easier, in the same way as the inclusion of traces, breakpoints, and assertions prepares a program for its quality assurance tests.
- Publication
Parallel Processing Letters, 1998, Vol 8, Issue 4, p421
- ISSN
0129-6264
- Publication type
Article
- DOI
10.1142/S0129626498000432