THE OBSERVATION: AN ABSTRACT COMMUNICATION MECHANISM
Michel Charpentier, Mamoun Filali, Philippe Mauran, Gérard Padiou, Philippe Quéinnec · Parallel Processing Letters · 1999
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.