Abstraction-Based Guided Search for Hybrid Systems
Sergiy Bogomolov, Alexandre Donze, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski, Martin Wehrle

Citation
Sergiy Bogomolov, Alexandre Donze, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski, Martin Wehrle. "Abstraction-Based Guided Search for Hybrid Systems". Proceedings of International SPIN Symposium on Model Checking of Software 2013, July, 2013.

Abstract
Hybrid systems represent an important and powerful formalism for modeling real-world applications such as embedded systems. A verification tool like SpaceEx is based on the exploration of a symbolic search space (the region space). As a verification tool, it is typically optimized towards proving the absence of errors. In some settings, e.g., when the verification tool is employed in a feedback-directed design cycle, one would like to have the option to call a version that is optimized towards finding an error path in the region space. A recent approach in this direction is based on guided search. Guided search relies on a cost function that indicates which states are promising to be explored, and preferably explores more promising states first. In this paper, an abstraction-based cost function based on pattern databases for guiding the reachability analysis is proposed. For this purpose, a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms is introduced. The new cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. The approach has been implemented in the SpaceEx model checker. The evaluation shows its practical potential.

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

  Sergiy Bogomolov, Alexandre Donze, Goran Frehse, Radu Grosu,
  Taylor T. Johnson, Hamed Ladan, Andreas Podelski, Martin
  Wehrle. <a
  href="http://www.terraswarm.org/pubs/60.html"
  >Abstraction-Based Guided Search for Hybrid
  Systems</a>, Proceedings of International SPIN
  Symposium on Model Checking of Software 2013, July, 2013.

• Plain text

  Sergiy Bogomolov, Alexandre Donze, Goran Frehse, Radu Grosu,
  Taylor T. Johnson, Hamed Ladan, Andreas Podelski, Martin
  Wehrle. "Abstraction-Based Guided Search for Hybrid
  Systems". Proceedings of International SPIN Symposium
  on Model Checking of Software 2013, July, 2013.

• BibTeX

  @inproceedings{BogomolovDonzeFrehseGrosuJohnsonLadanPodelskiWehrle13_AbstractionBasedGuidedSearchForHybridSystems,
      author = {Sergiy Bogomolov and Alexandre Donze and Goran
                Frehse and Radu Grosu and Taylor T. Johnson and
                Hamed Ladan and Andreas Podelski and Martin Wehrle},
      title = {Abstraction-Based Guided Search for Hybrid Systems},
      booktitle = {Proceedings of International SPIN Symposium on
                Model Checking of Software 2013},
      month = {July},
      year = {2013},
      abstract = {Hybrid systems represent an important and powerful
                formalism for modeling real-world applications
                such as embedded systems. A verification tool like
                SpaceEx is based on the exploration of a symbolic
                search space (the region space). As a verification
                tool, it is typically optimized towards proving
                the absence of errors. In some settings, e.g.,
                when the verification tool is employed in a
                feedback-directed design cycle, one would like to
                have the option to call a version that is
                optimized towards finding an error path in the
                region space. A recent approach in this direction
                is based on guided search. Guided search relies on
                a cost function that indicates which states are
                promising to be explored, and preferably explores
                more promising states first. In this paper, an
                abstraction-based cost function based on pattern
                databases for guiding the reachability analysis is
                proposed. For this purpose, a suitable abstraction
                technique that exploits the flexible granularity
                of modern reachability analysis algorithms is
                introduced. The new cost function is an effective
                extension of pattern database approaches that have
                been successfully applied in other areas. The
                approach has been implemented in the SpaceEx model
                checker. The evaluation shows its practical
                potential.},
      URL = {http://terraswarm.org/pubs/60.html}
  }
  

Posted by Mila MacBain on 9 May 2013.