Decomposing Specifications of Concurrent Systems
Martı́n Abadi, Leslie Lamport · 1994
This article was typeset using a L a T E X document style provided by Elsevier. 2 Composite specifications arise in two ways: by composing given parts to form a larger system, and by decomposing a given system into smaller parts. These two situations call for two methods of writing component specifications that differ in their treatment of the component's environment. This difference in turn leads to different proof rules. Here, we consider only decomposition. When decomposing a specification, the environment of each component is assumed to be the other components, and is usually left implicit. To reason about a component, we must state what we are assuming about its environment, and then prove that this assumption is satisfied by the other components. The Decomposition Theorem of Section 5 provides the needed proof rule. It reduces the verification of a complex, low-level system to proving properties of a higher-level specification and properties of one low-level component at a time. Decomposing proofs in this way allows us to apply decision procedures to verifications that hitherto required completely hand-guided proofs [11]. In the next section, we examine the issues that arise in decomposition. Our discussion is informal, because we wish to show that these issues are fundamental, not artifacts of a particular programming language or formalism. Section 3 covers the formal preliminaries, Section 4 investigates a method of writing specifications of components, and Section 5 gives the Decomposition Theorem. Proofs appear in [4].