COMPOSITIONAL SPECIFICATION AND VERIFICATION OF DISTRIBUTED SYSTEMS

We present a method for specification and verification of distributed systems that communicate via asynchronous message passing. The method handles both safety and liveness properties. It is compositional, i.e., a specification of a composite system can be obtained from specifications of its components. Specifications are given as labeled transition systems with fairness properties, using a program-like notation with guarded multiple assignments. Compositionality is attained by partitioning the labels of a transition system into input events, which intuitively denote message receptions, and output events, which intuitively denote message transmissions. A specification denotes a set of allowed sequences of message transmissions and receptions, in analogy with the way finite automata are used as acceptors of finite strings. A lower-level specification implements a higher-level specification if all sequences allowed by the lower-level specification are also allowed by the higher-level one. We present a verification technique which reduces the problem of verifying the correctness of an implementation to classical verification conditions. Safety properties are verified by establishing a simulation relation between transition systems. Liveness properties are verified using methods for proving termination under fairness assumptions. Since specifications can be given at various levels of abstraction, the method is suitable in a development process where a detailed implementation is developed from an abstract specification through a sequence of refinement steps. As an application of the method, an algorithm by Thomas for updating a distributed database is specified and verified.