Citation
Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli. "Library-Based Scalable Refinement Checking for Contract-Based Design". Design Automation and Test in Europe (DATE), 24, March, 2014.

Abstract
Given a global specification contract and a system described by a composition of contracts, system verification reduces to checking that the composite contract refines the specification contract, i.e. that any implementation of the composite contract implements the specification contract and is able to operate in any environment admitted by it. Contracts are captured using high-level declarative languages, for example, linear temporal logic (LTL). In this case, refinement checking reduces to an LTL satisfiability checking problem, which can be very expensive to solve for large composite contracts. This paper proposes a scalable refinement checking approach that relies on a library of contracts and local refinement assertions.We propose an algorithm that, given such a library, breaks down the refinement checking problem into multiple successive refinement checks, each of smaller scale. We illustrate the benefits of the approach on an industrial case study of an aircraft electric power system, with up to two orders of magnitude improvement in terms of execution time.

Electronic downloads

• http://www.src.org/library/publication/p069123/. (Submission to SRC website)
• http://dx.doi.org/10.7873/DATE.2014.167
• antonio_date14.pdf · application/pdf · 545 kbytes. ("Camera Ready" Version)
• http://escholarship.org/uc/item/9fq0r0r8. (Link to eScholarship site)

• HTML

  Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis,
  Alberto Sangiovanni-Vincentelli. <a
  href="http://www.terraswarm.org/pubs/238.html"
  >Library-Based Scalable Refinement Checking for
  Contract-Based Design</a>, Design Automation and Test
  in Europe (DATE), 24, March, 2014.

• Plain text

  Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis,
  Alberto Sangiovanni-Vincentelli. "Library-Based
  Scalable Refinement Checking for Contract-Based
  Design". Design Automation and Test in Europe (DATE),
  24, March, 2014.

• BibTeX

  @inproceedings{IannopolloNuzzoTripakisSangiovanniVincentelli14_LibraryBasedScalableRefinementCheckingForContractBased,
      author = {Antonio Iannopollo and Pierluigi Nuzzo and Stavros
                Tripakis and Alberto Sangiovanni-Vincentelli},
      title = {Library-Based Scalable Refinement Checking for
                Contract-Based Design},
      booktitle = {Design Automation and Test in Europe (DATE)},
      day = {24},
      month = {March},
      year = {2014},
      abstract = {Given a global specification contract and a system
                described by a composition of contracts, system
                verification reduces to checking that the
                composite contract refines the specification
                contract, i.e. that any implementation of the
                composite contract implements the specification
                contract and is able to operate in any environment
                admitted by it. Contracts are captured using
                high-level declarative languages, for example,
                linear temporal logic (LTL). In this case,
                refinement checking reduces to an LTL
                satisfiability checking problem, which can be very
                expensive to solve for large composite contracts.
                This paper proposes a scalable refinement checking
                approach that relies on a library of contracts and
                local refinement assertions.We propose an
                algorithm that, given such a library, breaks down
                the refinement checking problem into multiple
                successive refinement checks, each of smaller
                scale. We illustrate the benefits of the approach
                on an industrial case study of an aircraft
                electric power system, with up to two orders of
                magnitude improvement in terms of execution time.},
      URL = {http://terraswarm.org/pubs/238.html}
  }
  

Posted by Barb Hoversten on 2 Jan 2014.
Groups: tools