Component interfaces with contracts on ports

Abstract

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 component framework satisfies itself the general laws of an interface theory (concerning the composition, refinement, and environment correctness notions). 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. As a particular instance 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 modal refinement and with a weak modal environment correctness notion. The modal approach is particularly useful to specify loose environment assumptions. © 2013 Springer-Verlag.