Abstract:

We propose a complete description and validation of the ATMR protocol within the UNITY formalism. An operational description using the UNITY programming notation is given as well as a specification of the main correctness properties in the UNITY temporal logic. This formal description helps to understand precisely the mechanisms this protocol involves. In particular, we have noted the use of an incorrect detection algorithm to generate reset slots. Nevertheless, a hand-made proof is given that shows the model satisfies the specification in spite of this spurious detection. Moreover, through this study, we apply a general development process based upon the UNITY formalism. During this process, a very important step consists in tuning a program in order to make the validation step easier, in the same way as the inclusion of traces, breakpoints, and so on prepares a program for its test.
Michel Charpentier <>
Last modified: Thu Feb 10 13:36:55 EST 2000