Citation
Stavros Tripakis, Ben Lickly, Tom Henzinger, Edward A. Lee. "A Theory of Synchronous Relational Interfaces". Technical report, UC Berkeley, UCB/EECS-2010-45, April, 2010; Published in ACM Transactions on Programming Languages and Systems (TOPLAS). Vol. 33, Issue 4, July 2011.

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.

Electronic downloads

• http://www.eecs.berkeley.edu/Pubs/TechRpts/2010/EECS-2010-45.html
• http://chess.eecs.berkeley.edu/pubs/650.html. (Previous version of this work)
• http://dx.doi.org/10.1145/1985342.1985345

• HTML

  Stavros Tripakis, Ben Lickly, Tom Henzinger, Edward A. Lee.
  <a
  href="http://chess.eecs.berkeley.edu/pubs/666.html"
  ><i>A Theory of Synchronous Relational
  Interfaces</i></a>, Technical report,  UC
  Berkeley, UCB/EECS-2010-45, April, 2010; Published in ACM
  Transactions on Programming Languages and Systems (TOPLAS).
  Vol. 33, Issue 4, July 2011.

• Plain text

  Stavros Tripakis, Ben Lickly, Tom Henzinger, Edward A. Lee.
  "A Theory of Synchronous Relational Interfaces".
  Technical report,  UC Berkeley, UCB/EECS-2010-45, April,
  2010; Published in ACM Transactions on Programming Languages
  and Systems (TOPLAS). Vol. 33, Issue 4, July 2011.

• BibTeX

  @techreport{TripakisLicklyHenzingerLee10_TheoryOfSynchronousRelationalInterfaces,
      author = {Stavros Tripakis and Ben Lickly and Tom Henzinger
                and Edward A. Lee},
      title = {A Theory of Synchronous Relational Interfaces},
      institution = {UC Berkeley},
      number = {UCB/EECS-2010-45},
      month = {April},
      year = {2010},
      note = {Published in ACM Transactions on Programming
                Languages and Systems (TOPLAS). Vol. 33, Issue 4,
                July 2011.},
      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.},
      URL = {http://chess.eecs.berkeley.edu/pubs/666.html}
  }
  

Posted by Stavros Tripakis on 23 Apr 2010.
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.