(Inter-)Action Refinement: The Easy Way

Abstract

We outline and illustrate a formal concept for the specification and refinement of networks of interactive components. We describe systems by modular, functional specification techniques. We distinguish between black box and glass box views of interactive system components as well as refinements of their black box and glass box views. We identify and discuss several classes of refinements such as behaviour refinement, communication history refinement, interface interaction refinement, state space refinement, distribution refinement, and others. In particular, we demonstrate how these concepts of refinement and their verification are supported by functional specification techniques leading to a general formal refinement calculus. It can be used as the basis for a method for the development of distributed interactive systems.