Consistency and Composition of Process Specifications

Formal methods for the specification and development of distributed systems have traditionally supported a top-down, linear development process. However, there is a growing awareness in the (distributed) software engineering community that, in addition to a `vertical' structuring into design phases and steps, the specification and development of complex systems should also be structured `horizontally' according to, so called, viewpoints. Such multi-viewpoint development methods raise two important new issues though, viz. consistency and composition of viewpoint specifications. The aim of this thesis is to provide formal techniques to support multi-viewpoint specification and development. In particular, it deals with process algebraic techniques for viewpoint specification, consistency checking and viewpoint composition. An important issue is the formal definition of consistency, in particular when different viewpoints are expressed using different specification techniques -- a situation that is referred to as unbalanced (as opposed to balanced) consistency. To this end, a mathematical framework for formal, viewpoint oriented system development is elaborated by abstracting from specific viewpoint models and specific formal techniques. A number of existing process algebraic specification techniques based on, so called, implementation relations, are investigated on their suitability for viewpoint specification. The thesis contains a comprehensive study of all possible binary consistency relations between specifications in these techniques, resulting in a spectrum of consistency relations. It also provides techniques for composition in these specification techniques. In addition, a new mixed term specification technique is developed that combines the expressiveness of modal logics with the structuring capabilities of process calculi. Consistency and composition turn out to have precisely the desired properties, which makes it an ideal formalism for partial process specification. Moreover, because of its expressiveness, it can serve as a pivotal formalism for unbalanced consistency checking.