Library-Based Scalable Refinement Checking for Contract-Based Design
Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli

Citation
Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis, Alberto Sangiovanni-Vincentelli. "Library-Based Scalable Refinement Checking for Contract-Based Design". Talk or presentation, November, 2013; Poster presented at the 2013 TerraSwarm Annual Meeting.

Abstract
Contract-based design (CBD) is currently emerging as a paradigm to harness the complexity of system design by enabling compositional reasoning, hierarchical design and component reuse. In CBD, components are specified by contracts and systems by compositions of contracts. A contract denotes both a set of components that implement a specification and a set of environments in which it can operate. 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. Devising algorithms for efficient refinement checking is therefore key to the successful deployment of a contract-based methodology. In several applications, contracts are captured using high-level declarative languages, such as 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 due to the well known state explosion problem. This paper proposes a scalable refinement checking approach that relies on a library of contracts and local refinement assertions. We propose an algorithm which, 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, showing up to two orders of magnitude improvement in terms of execution time.

Electronic downloads

Internal. This publication has been marked by the author for TerraSwarm-only distribution, so electronic downloads are not available without logging in.

Citation formats

• HTML

  Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis,
  Alberto Sangiovanni-Vincentelli. <a
  href="http://www.terraswarm.org/pubs/234.html"><i>Library-Based
  Scalable Refinement Checking for Contract-Based
  Design</i></a>, Talk or presentation,  November,
  2013; Poster presented at the <a
  href="http://www.terraswarm.org/conferences/13/annual"
  >2013 TerraSwarm Annual Meeting</a>.

• Plain text

  Antonio Iannopollo, Pierluigi Nuzzo, Stavros Tripakis,
  Alberto Sangiovanni-Vincentelli. "Library-Based
  Scalable Refinement Checking for Contract-Based
  Design". Talk or presentation,  November, 2013; Poster
  presented at the <a
  href="http://www.terraswarm.org/conferences/13/annual"
  >2013 TerraSwarm Annual Meeting</a>.

• BibTeX

  @presentation{IannopolloNuzzoTripakisSangiovanniVincentelli13_LibraryBasedScalableRefinementCheckingForContractBased,
      author = {Antonio Iannopollo and Pierluigi Nuzzo and Stavros
                Tripakis and Alberto Sangiovanni-Vincentelli},
      title = {Library-Based Scalable Refinement Checking for
                Contract-Based Design},
      month = {November},
      year = {2013},
      note = {Poster presented at the <a
                href="http://www.terraswarm.org/conferences/13/annual"
                >2013 TerraSwarm Annual Meeting</a>.},
      abstract = {Contract-based design (CBD) is currently emerging
                as a paradigm to harness the complexity of system
                design by enabling compositional reasoning,
                hierarchical design and component reuse. In CBD,
                components are specified by contracts and systems
                by compositions of contracts. A contract denotes
                both a set of components that implement a
                specification and a set of environments in which
                it can operate. 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.
                Devising algorithms for efficient refinement
                checking is therefore key to the successful
                deployment of a contract-based methodology. In
                several applications, contracts are captured using
                high-level declarative languages, such as 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 due to the well known
                state explosion problem. This paper proposes a
                scalable refinement checking approach that relies
                on a library of contracts and local refinement
                assertions. We propose an algorithm which, 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, showing up to two orders of
                magnitude improvement in terms of execution time.},
      URL = {http://terraswarm.org/pubs/234.html}
  }
  

Posted by Antonio Iannopollo on 13 Dec 2013.