Aditya Zutshi
Sriram Sankaranarayanan
ABSTRACT
We present a search technique to falsify safety properties of hybrid systems that model a software system controlling a physical plant. Our approach takes as input (a) the controller code and (b) a plant model given as a black-box system that can be simulated for given inputs over finite time horizons. Our approach combines the symbolic execution of the controller software with an abstraction of the plant, which is discovered on-the-fly using simulations. This process is used to find abstract counterexamples to the safety properties of interest. The plant abstraction is then refined iteratively using the abstract counterexamples until a concrete violation is discovered. Empirical evaluation of our approach shows its promise in treating controller software, whose semantics are well-understood using formal techniques while using numerical simulations to produce abstractions of the underlying plant model, which is often an approximation of the actual plant.
- A. Bhatia and E. Frazzoli. Incremental search methods for reachability analysis of continuous and hybrid systems. Proc. of HSCC, pages 451--471, 2004.Google Scholar
Cross Ref
- S. Bogomolov, A. Donzé, G. Frehse, R. Grosu, T. T. Johnson, H. Ladan, A. Podelski, and M. Wehrle. Abstraction-based guided search for hybrid systems. In Model Checking Software, pages 117--134. Springer, 2013.Google ScholarCross Ref
- X. Chen, E. Abraham, and S. Sankaranarayanan. Flow<sup>*</sup>: An analyzer for non-linear hybrid systems. In International Conference on Computer Aided Verification (CAV), 2013.Google ScholarCross Ref
- A. Donzé and O. Maler. Systematic simulation using sensitivity analysis. Proc. of HSCC, pages 174--189, 2007. Google ScholarDigital Library
- G. Frehse, C. Le Guernic, A. Donzé, S. Cotton, R. Ray, O. Lebeltel, R. Ripado, A. Girard, T. Dang, and O. Maler. Spaceex: Scalable verification of hybrid systems. In Computer Aided Verification, pages 379--395. Springer, 2011. Google ScholarCross Ref
- J. Kapinski, B. H. Krogh, O. Maler, and O. Stursberg. On systematic simulation of open continuous systems. In Hybrid Systems: Computation and Control, pages 283--297. Springer, 2003. Google ScholarCross Ref
- T. Nahhal and T. Dang. Test coverage for continuous and hybrid systems. In Computer Aided Verification, pages 449--462, 2007. Google ScholarDigital Library
- A. Zutshi, S. Sankaranarayanan, J. V. Deshmukh, and J. Kapinski. Multiple shooting, cegar-based falsification for hybrid systems. In Proceedings of the 14th International Conference on Embedded Software, page 5. ACM, 2014. Google ScholarDigital Library
Index Terms
- Falsification of safety properties for closed loop control systems
Recommendations
Model Checking Safety Properties of Servo-Loop Control Systems
DSN '02: Proceedings of the 2002 International Conference on Dependable Systems and NetworksThis paper presents the experiences of using a symbolic model checker to check the safety properties of a servo-loop control system. Symbolic model checking has been shown to be beneficial when the system under analysis can be modeled as a finite state ...
Falsification of LTL safety properties in hybrid systems
This paper develops a novel approach for the falsification of safety properties given by a syntactically safe linear temporal logic (LTL) formula $${\phi}$$ for hybrid systems with nonlinear dynamics and input controls. When the hybrid system is unsafe, ...
Abstraction for falsification
CAV'05: Proceedings of the 17th international conference on Computer Aided VerificationAbstraction is traditionally used in the process of verification. There, an abstraction of a concrete system is sound if properties of the abstract system also hold in the concrete system. Specifically, if an abstract state a satisfies a property ψ then ...
Comments