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.

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.