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

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-60

May 10, 2009

http://www2.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.

---

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},
    Year= {2009},
    Month= {May},
    Url= {http://www2.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://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-60.html
%F Tripakis:EECS-2009-60