Abstract:
Hybrid systems represent an important and powerful formalism for modeling real-world applications that require both discrete and continuous behavior. A verification tool such as 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, we introduce an abstraction-based cost function based on pattern databases for guiding the reachability analysis. For this purpose, we introduce a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms. Our cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. We have implemented our approach in the SpaceEx model checker. Our evaluation shows its practical potential.
Reference:
Sergiy Bogomolov, Alexandre Donze, Goran Frehse, Radu Grosu, Taylor T. Johnson, Hamed Ladan, Andreas Podelski, Martin Wehrle, "Abstraction-Based Guided Search for Hybrid Systems", In Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN 2013), Stony Brook, New York, USA, pp. , 2013, jul.
Bibtex Entry:
@inproceedings{bogomolov2013spin,
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},
year = {2013},
booktitle = {Proceedings of the 20th International SPIN Symposium on Model Checking of Software (<a href="http://spin2013.cs.sunysb.edu/">SPIN 2013</a>)},
address = {Stony Brook, New York, USA},
month = jul,
pages = {},
doi = {10.1007/978-3-642-39176-7_8},
gsid = {9142077756418010202},
abstract = {Hybrid systems represent an important and powerful formalism for modeling real-world applications that require both discrete and continuous behavior. A verification tool such as 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, we introduce an abstraction-based cost function based on pattern databases for guiding the reachability analysis. For this purpose, we introduce a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms. Our cost function is an effective extension of pattern database approaches that have been successfully applied in other areas. We have implemented our approach in the SpaceEx model checker. Our evaluation shows its practical potential.},
pdf = {http://www.taylortjohnson.com/research/bogomolov2013spin.pdf},
}