This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)
The authors present a simulation-based bounded-horizon verification framework for hybrid systems with Lipschitz continuity on the continuous dynamics. In this framework, the bounded initial set is covered by a finite set of representative states, whose forward simulations are used to generate an over-approximation of all the reachable states. A novel feature of the proposed approach is that the representative states are generated dynamically, on-the-fly, along with the forward simulations. This key innovation refines the current ‘reachability-face’ by a new partition only when needed. This approach works for hybrid systems with state-triggered discrete jumps and allows piecewise constant bounded inputs, extending the existing work applied to switched systems with neither state-triggered discrete jumps nor inputs. Additionally, when the continuous dynamics is incremental (input-to-state) stable, the algorithm uses a simple Lipschitz-based discrepancy function to provide a constant error bound of over-approximation. This is of practical significance since a Lipschitz-based discrepancy function is easily computable, while a more precise discrepancy function may not be available. Because of the constant error bound, the number of representative simulations also converges to a constant. A prototype verifier, HS 3 V, has been developed, implementing the proposed algorithms and providing verification results from several benchmarks for performance demonstration.
References
-
-
1)
-
3. Chen, X., Abraham, E., Sankaranarayanan, S.: ‘Taylor model flowpipe construction for non-linear hybrid systems’. Proc. on Real-Time Systems Symp., San Juan, Puerto Rico, 2012.
-
2)
-
31. Bak, S., Bogomolov, S., Johnson, T.T.: ‘HYST: a source transformation and translation tool for hybrid automaton models’. Proc. of the 18th Int. Conf. on Hybrid Systems: Computation and Control, Seattle, Washington, USA, 2015, pp. 128–133.
-
3)
-
32. Althoff, M., Yaldiz, S., Rajhans, A., et al: ‘Formal verification of phase-locked loops using reachability analysis and continuization’. Int. Conf. on Computer-Aided Design, San Jose, CA, USA, 2011, pp. 659–666.
-
4)
-
7. Donzé, A., Maler, O.: ‘Systematic simulation using sensitivity analysis’. Int. Workshop on Hybrid Systems: Computation and Control, Pisa, Italy, 2007, pp. 174–189.
-
5)
-
30. Bak, S., Johnson, T.T.: ‘Periodically-scheduled controller analysis using hybrid systems reachability and continuization’. , 2015.
-
6)
-
5. Ren, H., Huang, J., Jiang, S., et al: ‘A new abstraction-refinement based verifier for modular linear hybrid automata and its implementation’. Proc. of the 11th Int. Conf. on Networking, Sensing and Control, Miami, FL, USA, 2014, pp. 30–35.
-
7)
-
13. Althoff, M., Stursberg, O., Buss, M.: ‘Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization’. 47th IEEE Conf. on Decision and Control, Cancun, Mexico, 2008, pp. 4042–4048.
-
8)
-
22. Kumar, R., Zhou, C., Jiang, S.: ‘Safety and transition-structure preserving abstraction of hybrid systems with inputs/outputs’. 9th Int. Workshop on Discrete Event Systems, Goteborg, Sweden, 2008, pp. 206–211.
-
9)
-
26. Angeli, D.: ‘A Lyapunov approach to incremental stability properties’, IEEE Trans. Autom. Control, 2002, 47, pp. 410–421.
-
10)
-
1. Chutinan, A., Krogh, B.H.: ‘Computational techniques for hybrid system verification’, IEEE Trans. Autom. Control, 2003, 48, pp. 64–75.
-
11)
-
18. Kapinski, J., Deshmukh, J.V., Sankaranarayanan, S., et al: ‘Simulation-guided lyapunov analysis for hybrid dynamical systems’. Proc. of the 17th Int. Conf. on Hybrid Systems: Computation and Control, Berlin, Germany, 2014, pp. 133–142.
-
12)
-
8. Clarke, E.M., Zuliani, P.: ‘Statistical model checking for cyber-physical systems’. Int. Symp. on Automated Tech. for Verification and Analysis, Taipei, Taiwan, 2011, pp. 1–12.
-
13)
-
23. Strzeboński, A.: ‘Computation with semialgebraic sets represented by cylindrical algebraic formulas’. Proc. Int. Symp. on Symbolic and Algebraic Computation, Munich, Germany, 2010.
-
14)
-
21. Ren, H., Kumar, R.: ‘Step simulation/over approximation-based verification of nonlinear deterministic hybrid system with inputs’. Proc. 5th IFAC Conf. on Analysis and Design of Hybrid Systems, Atlanta, GA, USA, 2015.
-
15)
-
9. Duggirala, P. S., Mitra, S., Viswanathan, M.: ‘Verification of annotated models from executions’. Proc. 2014 ACM Int. Conf. on Embedded Software, New Delhi, India, 2013, pp. 26.
-
16)
-
17)
-
2. Frehse, G., Le-Guernic, C., Donzé, A., et al: ‘Spaceex: scalable verification of hybrid systems’. Proc. Int. Conf. on Computer Aided Verification, Snowbird, UT, USA, 2011, pp. 379–395.
-
18)
-
15. Maidens, J., Arcak, M.: ‘Reachability analysis of nonlinear systems using matrix measures’, IEEE Trans. Autom. Control, 2015, 60, pp. 265–270.
-
19)
-
6. Ren, H., Huang, J., Jiang, S., et al: ‘Verification using counterexample fragment based specification relaxation: case of modular/concurrent linear hybrid automata’, IET Cyber-Phys. Syst., Theory Appl., 2017, 2, pp. 65–74.
-
20)
-
21)
-
17. Fan, C., Mitra, S.: ‘Bounded verification with on-the-fly discrepancy computation’. Int. Symp. on Automated Technology for Verification and Analysis, Shanghai, China, 2015, pp. 446–463.
-
22)
-
11. Huang, Z., Mitra, S.: ‘Proofs from simulations and modular annotations’. Proc. of the 17th Int. Conf. on Hybrid Systems: Computation and Control, Berlin, Germany, 2014, pp. 183–192.
-
23)
-
20. Wood, G., Zhang, B.: ‘Estimation of the Lipschitz constant of a function’, J. Global Optim., 1996, 8, pp. 91–103.
-
24)
-
19. Fan, C., Kapinski, J., Jin, X., et al: ‘Locally optimal reach set over-approximation for nonlinear systems’. Proc. Int. Conf. on Embedded Software, Pittsburgh, PA, USA, 2016, pp. 1–10.
-
25)
-
4. Jiang, S.: ‘Reachability analysis of linear hybrid automata by using counterexample fragment based abstraction refinement’. Proc. on American Control Conf., New York City, USA, 2007.
-
26)
-
14. Althoff, M., Stursberg, O., Buss, M.: ‘Implementation of interval arithmetic in CORA 2016’. , 2016, pp. 91–105.
-
27)
-
28)
-
25. Ren, H., Kumar, R.: ‘Simulation-based verification of bounded-horizon safety for hybrid systems using dynamic number of simulations: extended version’, 2018. .
-
29)
-
12. Henzinger, T.A., Ho, P.H., Wong-Toi, H.: ‘Hytech: the next generation’. Proc. of the 16th IEEE Real-Time Systems Symp., Pisa, Italy, 1995, pp. 56–65.
-
30)
-
16. Fan, C., Qi, B., Mitra, S., et al: ‘Automatic reachability analysis for nonlinear hybrid models with C2E2’. Int. Conf. Computer-Aided Verification, Toronto, Ontario, Canada, 2016, pp. 531–538.
-
31)
-
10. Huang, Z., Mitra, S.: ‘Computing bounded reach sets from sampled simulation traces’. Proc. Int. Conf. on Hybrid Systems: Computation and Control, Beijing, China, 2012, pp. 291–294.
-
32)
-
24. Mørken, K.: ‘Numerical solution of differential equations’, 2010. .
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2018.5017
Related content
content/journals/10.1049/iet-cps.2018.5017
pub_keyword,iet_inspecKeyword,pub_concept
6
6