Structured Specification of Communicating Systems

Abstract

Specification methods for distributed systems is the underlying theme of this paper. A model of communicating processes with rendezvous interactions is assumed as a basis for the discussion. The possible interactions by a process, and the interconnection between several subprocesses within a process are specified using the concept of ports, which are specified separately. Step-wise refinement of process specifications and associated verification rules are considered. The step-wise refinement of port specifications and associated interactions is considered as well. After the presentation of an introductory example, the paper discusses the basic concepts of the specification method. They are then applied to more complex examples. The step-wise wefinement of ports and interactions is demonstrated by a hardware interface for which an abstract specification and a more detailed implementation is given. Proof rules for verifying the consistency of detailed and more abstract specifications are discussed in some detail.