Your browser does not support JavaScript!
http://iet.metastore.ingenta.com
1887

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

Loading full text...

Full text loading...

/deliver/fulltext/iet-cps/4/3/IET-CPS.2018.5017.html;jsessionid=15iz1vmoxwpih.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2018.5017&mimeType=html&fmt=ahah

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. 128133.
    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. 659666.
    4. 4)
      • 7. Donzé, A., Maler, O.: ‘Systematic simulation using sensitivity analysis’. Int. Workshop on Hybrid Systems: Computation and Control, Pisa, Italy, 2007, pp. 174189.
    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. 3035.
    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. 40424048.
    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. 206211.
    9. 9)
      • 26. Angeli, D.: ‘A Lyapunov approach to incremental stability properties’, IEEE Trans. Autom. Control, 2002, 47, pp. 410421.
    10. 10)
      • 1. Chutinan, A., Krogh, B.H.: ‘Computational techniques for hybrid system verification’, IEEE Trans. Autom. Control, 2003, 48, pp. 6475.
    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. 133142.
    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. 112.
    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. 379395.
    18. 18)
      • 15. Maidens, J., Arcak, M.: ‘Reachability analysis of nonlinear systems using matrix measures’, IEEE Trans. Autom. Control, 2015, 60, pp. 265270.
    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. 6574.
    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. 446463.
    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. 183192.
    23. 23)
      • 20. Wood, G., Zhang, B.: ‘Estimation of the Lipschitz constant of a function’, J. Global Optim., 1996, 8, pp. 91103.
    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. 110.
    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’. [email protected], 2016, pp. 91105.
    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. 5665.
    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. 531538.
    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. 291294.
    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.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2018.5017
Loading

Related content

content/journals/10.1049/iet-cps.2018.5017
pub_keyword,iet_inspecKeyword,pub_concept
6
6
Loading
This is a required field
Please enter a valid email address