Citation
Pierluigi Nuzzo, Antonio Iannopollo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli. "Are Interface Theories Equivalent to Contract Theories?". International Conference on Formal Methods and Models for Co-Design (MEMOCODE), 19, October, 2014.

Abstract
Contract-based design is emerging as a unifying compositional paradigm for the specification, design and verification of large-scale complex systems. Different contract frameworks are currently available, but we lack a clear understanding of the relations between them. In this paper, we investigate the relation between interface theories (specifically, relational interfaces) and assume-guarantee (A/G) contracts. We introduce a natural transformation of interfaces to A/G contracts represented by linear temporal logic. Then, we analyze differences and correspondences between key operators and relations in the two theories (i.e. composition, refinement and conjunction), by studying their preservation properties under the proposed transformation. We show that the transformation preserves refinement, but does not generally preserve serial composition and conjunction. Then, we present an assumption-projection operator to make it possible to preserve serial composition and compatibility checking. Finally, we provide illustrative examples that shed light on the effectiveness of both frameworks for requirement formalization, early detection of integration errors, and use of abstraction-refinement.

Electronic downloads

• https://www.src.org/library/publication/p071769/. (Link to paper on SRC website.)
• http://dx.doi.org/10.1109/MEMCOD.2014.6961848

• HTML

  Pierluigi Nuzzo, Antonio Iannopollo, Stavros Tripakis,
  Alberto Sangiovanni-Vincentelli. <a
  href="http://www.terraswarm.org/pubs/353.html"
  >Are Interface Theories Equivalent to Contract
  Theories?</a>, International Conference on Formal
  Methods and Models for Co-Design (MEMOCODE), 19, October,
  2014.

• Plain text

  Pierluigi Nuzzo, Antonio Iannopollo, Stavros Tripakis,
  Alberto Sangiovanni-Vincentelli. "Are Interface
  Theories Equivalent to Contract Theories?".
  International Conference on Formal Methods and Models for
  Co-Design (MEMOCODE), 19, October, 2014.

• BibTeX

  @inproceedings{NuzzoIannopolloTripakisSangiovanniVincentelli14_AreInterfaceTheoriesEquivalentToContractTheories,
      author = {Pierluigi Nuzzo and Antonio Iannopollo and Stavros
                Tripakis and Alberto Sangiovanni-Vincentelli},
      title = {Are Interface Theories Equivalent to Contract
                Theories?},
      booktitle = {International Conference on Formal Methods and
                Models for Co-Design (MEMOCODE)},
      day = {19},
      month = {October},
      year = {2014},
      abstract = {Contract-based design is emerging as a unifying
                compositional paradigm for the specification,
                design and verification of large-scale complex
                systems. Different contract frameworks are
                currently available, but we lack a clear
                understanding of the relations between them. In
                this paper, we investigate the relation between
                interface theories (specifically, relational
                interfaces) and assume-guarantee (A/G) contracts.
                We introduce a natural transformation of
                interfaces to A/G contracts represented by linear
                temporal logic. Then, we analyze differences and
                correspondences between key operators and
                relations in the two theories (i.e. composition,
                refinement and conjunction), by studying their
                preservation properties under the proposed
                transformation. We show that the transformation
                preserves refinement, but does not generally
                preserve serial composition and conjunction. Then,
                we present an assumption-projection operator to
                make it possible to preserve serial composition
                and compatibility checking. Finally, we provide
                illustrative examples that shed light on the
                effectiveness of both frameworks for requirement
                formalization, early detection of integration
                errors, and use of abstraction-refinement.},
      URL = {http://terraswarm.org/pubs/353.html}
  }
  

Posted by Barb Hoversten on 31 Aug 2014.
Groups: tools