World Scientific
Skip main navigation

Cookies Notification

We use cookies on this site to enhance your user experience. By continuing to browse the site, you consent to the use of our cookies. Learn More
×

System Upgrade on Tue, May 28th, 2024 at 2am (EDT)

Existing users will be able to log into the site and access content. However, E-commerce and registration of new users may not be available for up to 12 hours.
For online purchase, please visit us again. Contact us at customercare@wspc.com for any enquiries.

Specification and Verification of the ATMR Protocol Using UNITY: Part 2: Correctness Proof

    https://doi.org/10.1142/S0129626498000444Cited by:2 (Source: Crossref)

    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.