Interfaces for Component-Based Design
Stavros Tripakis1, Ben Lickly, Edward A. Lee and Thomas A. Henzinger
Center for Hybrid and Embedded Software Systems (CHESS), National Science Foundation 0720882, National Science Foundation 0720841, Army Research Office W911NF-07-2-0019, Air Force Office of Scientific Research FA9550-06-0312, Air Force Research Laboratory FA8750-08-2-0001, California MICRO, Agilent Technologies, Robert Bosch GmBH, Lockheed-Martin, National Instruments, Thales and Toyota
Component-based design has emerged as a significant challenge in building complex systems, such as embedded, cyber-physical systems, in an efficient and reliable manner. The size and complexity of such systems prohibits designing an entire system from scratch, or building it as a single unit. Instead, the system must be designed as a set of components, some built from scratch, some inherited by legacy. Interfaces play a key role in component-based design, as they provide the means to reason about components. An interface can be seen as an abstraction of a component: on one hand, such an abstraction captures information that is essential in order to use the component in a given context; on the other hand, the abstraction hides unnecessary information, making reasoning simpler and more efficient.
Significant progress has been made in the past several years toward the development of a comprehensive theory of interfaces for component-based design. In particular, such a theory has been developed in a series of papers by De Alfaro, Henzinger et al. Yet, despite the advances, this theory is far from being complete. This project seeks to further study interfaces with the aim of gaining a better understanding of some of the missing pieces of the puzzle.
As a first step, we have been working on extending the theory toward so-called relational interfaces, that is, interfaces that specify relations between inputs and outputs . Consider, for example, a component that is supposed to take as input a number n>0 and return as output n+1. The interface for such a component cannot be captured by existing theories. We have developed a theory where input-output relations can be captured. Our theory supports both stateless and stateful interfaces, includes explicit notions of environments and pluggability, and satisfies fundamental properties such as preservation of refinement by composition, and characterization of pluggability by refinement.
- EECS Technical Report: On Relational Interfaces