Compositional Refinement of Interactive Systems

We describe systems and their components by functional specification techniques. We define notions of interface and interaction refinement for interactive systems and their components. These notions of refinement allow one to change both the syntactic (the number of channels and sorts of messages at the channels) and the semantic interface (causality flow between messages and interaction granularity) of an interactive system component. We prove that these notions of refinement are compositional with respect to sequential and parallel composition of system components, communication feedback and recursive declarations of system components. According to these proofs refinements of networks can be accomplished in a modular way by refining their components. We generalize the notions of refinement to refining contexts. Finally full abstraction for specifications is defined and compositionality with respect to this abstraction is shown, too. This work was partially sponsored by the German S..