Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
4951774 | Science of Computer Programming | 2017 | 46 Pages |
Abstract
We present a counterexample-guided abstraction refinement ( CEGAR) approach for the verification of safety properties of linear hybrid automata with large discrete state spaces, such as naturally arising when incorporating health state monitoring and degradation levels into the controller design. Such models can - in contrast to purely functional controller models - not be analyzed with hybrid verification engines relying on explicit representations of modes, but require fully symbolic representations for both the continuous and discrete part of the state space. The presented abstraction methods directly work on a symbolic representation of arbitrary non-convex combinations of linear constraints and boolean variables using LinAIGs. Several interpolation methods allow us to compute abstractions consisting of fewer linear constraints, and hence reduce the complexity of the reachable state set computation. In combination with methods that guarantee the preciseness of abstractions, this leads to a significant reduction of the runtimes of the verification process compared with exact verification.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ernst Althaus, Björn Beber, Werner Damm, Stefan Disch, Willem Hagemann, Astrid Rakow, Christoph Scholl, Uwe Waldmann, Boris Wirtz,