Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

On Relational Interfaces

Stavros Tripakis, Ben Lickly, Thomas A. Henzinger and Edward A. Lee

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2009-60
May 10, 2009

http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-60.pdf

In this paper we extend the work of De Alfaro, Henzinger et al, on interface theories for component-based design. Existing interface theories fail to capture functional relations between the inputs and outputs of an interface. For example, a simple interface that takes as input a number n>0 and returns as output n+1, cannot be expressed in existing theories. In this paper we provide a theory of relational interfaces, where such 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. We achieve these properties by making reasonable restrictions on feedback loops in interface compositions.

Author Comments: This paper has been published in EMSOFT 09, October, 2009.


BibTeX citation:

@techreport{Tripakis:EECS-2009-60,
    Author = {Tripakis, Stavros and Lickly, Ben and Henzinger, Thomas A. and Lee, Edward A.},
    Title = {On Relational Interfaces},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2009},
    Month = {May},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-60.html},
    Number = {UCB/EECS-2009-60},
    Note = {This paper has been published in <a href="http://chess.eecs.berkeley.edu/pubs/650.html">EMSOFT 09</a>, October, 2009.},
    Abstract = {In this paper we extend the work of De Alfaro, Henzinger et al, on interface theories for component-based design. Existing interface theories fail to capture functional relations between the inputs and outputs of an interface. For example, a simple interface that takes as input a number n>0 and returns as output n+1, cannot be expressed in existing theories. In this paper we provide a theory of relational interfaces, where such 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. We achieve these properties by making reasonable restrictions on feedback loops in interface compositions.}
}

EndNote citation:

%0 Report
%A Tripakis, Stavros
%A Lickly, Ben
%A Henzinger, Thomas A.
%A Lee, Edward A.
%T On Relational Interfaces
%I EECS Department, University of California, Berkeley
%D 2009
%8 May 10
%@ UCB/EECS-2009-60
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-60.html
%F Tripakis:EECS-2009-60