Data Entry: Please note that the research database will be replaced by UNIverse by the end of October 2023. Please enter your data into the system https://universe-intern.unibas.ch. Thanks

Login for users with Unibas email account...

Login for registered users without Unibas email account...

 
Abstraction-based guided search for hybrid systems
ConferencePaper (Artikel, die in Tagungsbänden erschienen sind)
 
ID 2315192
Author(s) Bogomolov, Sergiy; Donze, Alexandre; Frehse, Goran; Grosu, Radu; Johnson, Taylor T.; Ladan, Hamed; Podelski, Andreas; Wehrle, Martin
Author(s) at UniBasel Wehrle, Martin
Year 2013
Title Abstraction-based guided search for hybrid systems
Editor(s) Bartocci, Ezio; Ramakrishnan, C. R.
Book title (Conference Proceedings) Model checking software : proceedings of the 20th international SPIN symposium on model checking of software (SPIN 2013)
Place of Conference New York, USA
Publisher Springer
Place of Publication Heidelberg
Pages S. 117-134
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.
edoc-URL http://edoc.unibas.ch/dok/A6212196
Full Text on edoc No
Digital Object Identifier DOI 10.1007/978-3-642-39176-7_8
ISI-Number INSPEC:13536779
 
   

MCSS v5.8 PRO. 0.346 sec, queries - 0.000 sec ©Universität Basel  |  Impressum   |    
29/03/2024