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