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 ³ V, has been developed, implementing the proposed algorithms and providing verification results from several benchmarks for performance demonstration.

References

1. 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. 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. 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. 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. 5)
  - 30. Bak, S., Johnson, T.T.: ‘Periodically-scheduled controller analysis using hybrid systems reachability and continuization’. No. AFRL-RI-RS-TP-2016–002, Air Force Research La./Information Directorate ROME United States, 2015.
6. 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. 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. 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. 9)
  - 26. Angeli, D.: ‘A Lyapunov approach to incremental stability properties’, IEEE Trans. Autom. Control, 2002, 47, pp. 410–421.
10. 10)
  - 1. Chutinan, A., Krogh, B.H.: ‘Computational techniques for hybrid system verification’, IEEE Trans. Autom. Control, 2003, 48, pp. 64–75.
11. 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. 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. 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. 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. 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. 16)
  - 29. ‘Gnuplot’. Available at http://www.gnuplot.info/.
17. 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. 18)
  - 15. Maidens, J., Arcak, M.: ‘Reachability analysis of nonlinear systems using matrix measures’, IEEE Trans. Autom. Control, 2015, 60, pp. 265–270.
19. 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. 20)
  - 27. ‘ALGLIB’. Available at http://www.alglib.net.
21. 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. 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. 23)
  - 20. Wood, G., Zhang, B.: ‘Estimation of the Lipschitz constant of a function’, J. Global Optim., 1996, 8, pp. 91–103.
24. 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. 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. 26)
  - 14. Althoff, M., Stursberg, O., Buss, M.: ‘Implementation of interval arithmetic in CORA 2016’. ARCH@CPSWeek, 2016, pp. 91–105.
27. 27)
  - 28. ‘Clipper’. Available at http://www.angusj.com/delphi/clipper.php.
28. 28)
  - 25. Ren, H., Kumar, R.: ‘Simulation-based verification of bounded-horizon safety for hybrid systems using dynamic number of simulations: extended version’, 2018. Available at http://www.ece.iastate.edu/rkumar/PUBS/simverify-x.pdf.
29. 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. 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. 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. 32)
  - 24. Mørken, K.: ‘Numerical solution of differential equations’, 2010. Available at: http://www.uio.no/studier/emner/matnat/math/MAT-INF1100/h10/kompendiet/kap13.pdf.

Simulation-based verification of bounded-horizon safety for hybrid systems using dynamic number of simulations

References

Related content