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.
A termination detection algorithm: specification and verification
