Abstract:

We address the problem of studying and proving reactive and distributed programs within the UNITY framework. We consider parallel algorithms where different processes are concurrently executed. Moreover, we assume that the processes have an infinite behaviour (reaction) and that they share neither memory nor a common clock (distribution). The UNITY programming notation (fair transition systems) is used to describe these algorithms, and specifications and proofs are handled within the UNITY logic (temporal linear logic). In this context, we think that proof assistants are necessary. However, we believe that distribution must be precisely characterized in UNITY before we can efficiently use automatic provers. Two problems are more specifically explored: communication between processes and mapping to distributed architectures. We propose an abstract communication mechanism based on an observation relation between processes variables. The communication description provided by this mechanism is more abstract than the traditional message-passing model and allows a clear distinction between synchronization and pure communication. This abstraction of communication appears to be helpful to describe and prove distributed algorithms. We also define the product, a new UNITY operator which can be used to formalize the mapping of programs to distributed architectures. Using this operator, we prove that, in spite of UNITY interleaving semantics, the true parallelism of a distributed implementation preserves most of the properties satisfied by a program.
Michel Charpentier <>
Last modified: Thu Feb 10 13:36:50 EST 2000