*banner
 

A Theory of Synchronous Relational Interfaces
Stavros Tripakis, Ben Lickly, Tom Henzinger, Edward A. Lee

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

Citation formats  
  • 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.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

You are not logged in 
©2002-2014 Chess