An Abstract Account of Composition

act Account of Composition Mart n Abadi1 and Stephan Merz2 1 Digital Equipment Corporation, Systems Research Center, 130 Lytton Avenue, Palo Alto, CA 94301, U.S.A. 2 Institut fur Informatik, Technische Universitat Munchen, Arcisstr. 21, 80290 Munchen, Germany We present a logic of speci cations of reactive systems. The logic is independent of particular computational models, but it captures common patterns of reasoning with assumption-commitment speci cations. We use the logic for deriving proof rules for TLA and CTL speci cations. 1 Assumption-commitment speci cations Modularity is a central concern in the design of speci cation methods. In general terms, modularity is the ability to reduce reasoning about a complete system to reasoning about its components. These components are not expected to operate in fully arbitrary environments. In the context of the complete system, each component can assume that its environment is to some extent well behaved, for instance that it adheres to ce...

• Type: Conference
• Year: 1995
• Where: MFCS
• Authors: Martín Abadi, Stephan Merz
• Keywords: Assumption-commitment Speci Cation, MFCS 1995, Reactive Systems, Speci Cation, Theoretical Computer Science