A Theory of Reactive Components

We present a theory of reactive components. We identify a component by its provided services, and specify the individual services by a guarded-design, which enables one to separate the responsibility of clients from the commitment made by the component, and model the behaviour of a component by a set of failures and divergences. Protocols are introduced to coordinate the interactions between a component and its environment. We adopt the notion of process refinement to formalise the substitutivity of components, and provide a complete proof method based on the notion of simulations. We also study the algebraic properties of component combinators.