A UNITY-based Formalism for Dynamic Distributed Systems

摘要

We describe Dynamic UNITY, a new formalism for the specification of dynamic distributed systems based on the UNITY formalism. This formalism allows for the specification and proof of systems where processes may be created and destroyed, and where communication links among processes may change. It also introduces asynchronous messaging as a primitive construct, to facilitate the composition of multiple programs into a larger system. We also present an example Dynamic UNITY system that illustrates the dynamic aspects of the new formalism, and outline a correctness proof for the example.