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

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2010-45

April 23, 2010

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-45.pdf

In a component-based design context, we propose a relational interface theory for synchronous systems. A component is abstracted by its interface, which consists of input and output variables, as well as one or more contracts. A contract is a relation between input and output assignments. In the stateless case, there is a single contract that holds at every synchronous round. In the general, stateful, case, the contract may depend on the state, modeled as the history of past observations. Interfaces can be composed by connection or feedback. Parallel composition is a special case of connection. Feedback is allowed only for Moore interfaces, where the contract does not depend on the current values of the input variables that are connected (although it may depend on past values of such variables). The theory includes explicit notions of environments, pluggability and substitutability. Environments are themselves interfaces. Pluggability means that the closed-loop system formed by an interface and an environment is well-formed, that is, a state with unsatisfiable contract is unreachable. Substitutability means that an interface can replace another interface in any environment. A refinement relation between interfaces is proposed, that has two main properties: first, it is preserved by composition; second, it is equivalent to substitutability for well-formed interfaces. Shared refinement and abstraction operators, corresponding to greatest lower and least upper bounds with respect to refinement, are also defined. Input-complete interfaces, that impose no restrictions on inputs, and deterministic interfaces, that produce a unique output for any legal input, are discussed as special cases, and an interesting duality between the two classes is exposed. A number of illustrative examples are provided, as well as algorithms to compute compositions, check refinement, and so on, for finite-state interfaces.

---

BibTeX citation:

@techreport{Tripakis:EECS-2010-45,
    Author= {Tripakis, Stavros and Lickly, Ben and Henzinger, Thomas A. and Lee, Edward A.},
    Title= {A Theory of Synchronous Relational Interfaces},
    Year= {2010},
    Month= {Apr},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-45.html},
    Number= {UCB/EECS-2010-45},
    Abstract= {In a component-based design context, we propose a relational interface theory for synchronous systems. A component is abstracted by its interface, which consists of input and output variables, as well as one or more contracts. A contract is a relation between input and output assignments. In the stateless case, there is a single contract that holds at every synchronous round. In the general, stateful, case, the contract may depend on the state, modeled as the history of past observations. Interfaces can be composed by connection or feedback. Parallel composition is a special case of connection. Feedback is allowed only for Moore interfaces, where the contract does not depend on the current values of the input variables that are connected (although it may depend on past values of such variables). The theory includes explicit notions of environments, pluggability and substitutability. Environments are themselves interfaces. Pluggability means that the closed-loop system formed by an interface and an environment is well-formed, that is, a state with unsatisfiable contract is unreachable. Substitutability means that an interface can replace another interface in any environment. A refinement relation between interfaces is proposed, that has two main properties: first, it is preserved by composition; second, it is equivalent to substitutability for well-formed interfaces. Shared refinement and abstraction operators, corresponding to greatest lower and least upper bounds with respect to refinement, are also defined. Input-complete interfaces, that impose no restrictions on inputs, and deterministic interfaces, that produce a unique output for any legal input, are discussed as special cases, and an interesting duality between the two classes is exposed. A number of illustrative examples are provided, as well as algorithms to compute compositions, check refinement, and so on, for finite-state interfaces.},
}

EndNote citation:

%0 Report
%A Tripakis, Stavros 
%A Lickly, Ben 
%A Henzinger, Thomas A. 
%A Lee, Edward A. 
%T A Theory of Synchronous Relational Interfaces
%I EECS Department, University of California, Berkeley
%D 2010
%8 April 23
%@ UCB/EECS-2010-45
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-45.html
%F Tripakis:EECS-2010-45