We study interacting components and their compatibility with respect to synchronous and asynchronous composition. The behavior of components is formalized by I/O-transition systems. Synchronous composition is based on simultaneous execution of shared output and input actions of two components while asynchronous composition uses unbounded FIFO-buffers for message transfer. In both contexts we study compatibility notions based on the idea that any output issued by one component should be accepted as an input by the other. We distinguish between strong and weak versions of compatibility, the latter allowing the execution of internal actions before a message is accepted. We consider open systems and study conditions under which (strong/weak) synchronous compatibility is sufficient and necessary to get (strong/weak) asynchronous compatibility. We show that these conditions characterize half-duplex systems. Then we focus on the verification of weak asynchronous compatibility for possibly non half-duplex systems and provide a decidable criterion that ensures weak asynchronous compatibility. We investigate conditions under which this criterion is complete, i.e. if it is not satisfied then the asynchronous system is not weakly asynchronously compatible. Finally, we discuss deadlock-freeness and investigate relationships between deadlock-freeness in the synchronous and in the asynchronous case.

We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduces some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

Abstract. One of the most novel features of C ASL , the Common Algebraic Specification Language, is the provision of so-called architectural specifications for describing the modular structure of software systems. A brief discussion of refinement of C ASL specifications provides the setting for a presentation of the rationale behind architectural specifications. This is followed by some details of the features provided in C ASL for architectural specifications, hints concerning their semantics, and simple results justifying their usefulness in the development process.

We present an algebraic specification language (PLUSS) and a program construction method. Programs are built systematically from an algebraic specification of the data they deal with. The method was tested on a realistic problem (part of a telephone switching system). In these experiments, it turned out that error handling was the difficult part to specify and to program. This paper shows how to cope with this problem at the specification level and during the program development process.