A meta-theory for component interfaces with contracts on ports

• We show how to build a component theory on top of a labeled interface theory.
• Component interfaces are equipped with assume/guarantee ports.
• We show that refinement of component interface specifications is compositional.
• We provide methodological guidelines how to design reliable component interfaces.
• We consider two instantiations: modal I/O-transition systems and I/O-predicates.

We show how the abstract concept of a labeled interface theory can be canonically extended to an abstract framework for component interfaces with ports. The resulting theory satisfies itself the general laws of an interface theory for composition, refinement and communication compatibility. The ports of a component interface represent the interaction points of a component. Each port is equipped with a contract specifying the assumptions on and the guarantees for the environment of a component. We study reliable component interfaces and we provide methodological guidelines how to design reliable interfaces and how to adapt them to changing environments. Two instances of our approach are presented. First, we consider modal component interfaces such that component behaviors and the assume and guarantee behaviors of ports are given in terms of modal I/O-transition systems with weak notions of refinement and compatibility. The second instance uses I/O-predicates as interface specifications.