Abstract:
In this paper, we introduce an observation relation as an
abstraction of point-to-point communication in distributed
architectures. After showing how its semantics and syntax can be
embedded within the UNITY approach, we state general observation
properties. Finally, we consider the description and the validation
of a distributed mutual exclusion algorithm. The relevant aspect of
such a validation is the exclusive use of refinements and
observations properties for the proof of these refinements.
Michel Charpentier <
>
Last modified: Thu Feb 10 13:36:55 EST 2000