Loading...
Please wait, while we are loading the content...
Similar Documents
Assume-guarantee abstraction refinement meets hybrid systems
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Pasareanu, Corina S. Strump Sr., Thomas Grosu, Radu Greitschus Sr., Marius Bogomolov, Sergiy Podelski Sr., Andreas Frehse, Goran |
| Copyright Year | 2014 |
| Description | Compositional verification techniques in the assume- guarantee style have been successfully applied to transition systems to efficiently reduce the search space by leveraging the compositional nature of the systems under consideration. We adapt these techniques to the domain of hybrid systems with affine dynamics. To build assumptions we introduce an abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement. We have implemented our approach in the symbolic hybrid model checker SpaceEx. The evaluation shows its practical potential. To the best of our knowledge, this is the first work combining assume-guarantee reasoning with automatic abstraction-refinement in the context of hybrid automata. |
| File Size | 435334 |
| Page Count | 16 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_20150021848 |
| Archival Resource Key | ark:/13960/t8dg1rb6d |
| Language | English |
| Publisher Date | 2014-11-18 |
| Access Restriction | Open |
| Subject Keyword | Reliability Statistical Methods Model Checking Controllers Grid Refinement Mathematics Algorithms Automata Theory Assumptions Dynamic Models Systems Analysis Formalism Program Verification Computers Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Article |
