http://iet.metastore.ingenta.com
1887

access icon openaccess Reachability resolution for discrete-time hybrid systems with application to automated test generation for Simulink/Stateflow

  • HTML
    422.587890625Kb
  • PDF
    1.4869966506958008MB
  • XML
    276.662109375Kb
Loading full text...

Full text loading...

/deliver/fulltext/iet-cps/2/1/IET-CPS.2017.0007.html;jsessionid=1rkllexws2v24.x-iet-live-01?itemId=%2fcontent%2fjournals%2f10.1049%2fiet-cps.2017.0007&mimeType=html&fmt=ahah

References

    1. 1)
      • 1. Simulink/Stateflow, ‘https://www.mathworks.com/products/simulink.html’, [accessed: 23/02/2017].
        .
    2. 2)
    3. 3)
      • C. Zhou , R. Kumar .
        3. Zhou, C., Kumar, R.: ‘Modeling Simulink diagrams using input/output extended finite automata’. Annual Int. Computer Software and Applications Conf., 2009, vol. 2, pp. 462467.
        . Annual Int. Computer Software and Applications Conf. , 462 - 467
    4. 4)
    5. 5)
      • M. Li , R. Kumar .
        5. Li, M., Kumar, R.: ‘Stateflow to extended finite automata translation’. 2011 IEEE 35th Annual Computer Software and Applications Conf. Workshops (COMPSACW), July 2011, pp. 16.
        . 2011 IEEE 35th Annual Computer Software and Applications Conf. Workshops (COMPSACW) , 1 - 6
    6. 6)
      • M. Li , R. Kumar .
        6. Li, M., Kumar, R.: ‘Model-based automatic test generation for Simulink/Stateflow using extended finite automaton’. Proc. Eighth IEEE Int. Conf. on Automation Science and Engineering (CASE 2012), August 2012.
        . Proc. Eighth IEEE Int. Conf. on Automation Science and Engineering (CASE 2012)
    7. 7)
    8. 8)
      • M. Li , R. Kumar .
        8. Li, M., Kumar, R.: ‘Reduction of automated test generation for Simulink/Stateflow to reachability and its novel resolution’. Proc. Eighth IEEE Int. Conf. on Automation Science and Engineering (CASE 2013), August 2013.
        . Proc. Eighth IEEE Int. Conf. on Automation Science and Engineering (CASE 2013)
    9. 9)
      • R. Alur .
        9. Alur, R.: ‘Formal verification of hybrid systems’. 2011 Proc. Int. Conf. on Embedded Software (EMSOFT), October 2011, pp. 273278.
        . 2011 Proc. Int. Conf. on Embedded Software (EMSOFT) , 273 - 278
    10. 10)
      • J.-F. Raskin .
        10. Raskin, J.-F.: ‘Reachability problems for hybrid automata’. Reachability Problems, 2011 (LNCS, 6945), pp. 2830.
        . Reachability Problems , 28 - 30
    11. 11)
    12. 12)
      • T.A. Henzinger , P.-H. Ho , H. Wong-Toi .
        12. Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: ‘Hytech: a model checker for hybrid systems’. Int. Conf. on Computer Aided Verification, 1997, pp. 460463.
        . Int. Conf. on Computer Aided Verification , 460 - 463
    13. 13)
      • G. Frehse , C. Le Guernic , A. Donzé .
        13. Frehse, G., Le Guernic, C., Donzé, A., et al: ‘Spaceex: scalable verification of hybrid systems’. Int. Conf. on Computer Aided Verification, 2011, pp. 379395.
        . Int. Conf. on Computer Aided Verification , 379 - 395
    14. 14)
      • X. Chen , E. Ábrahám , S. Sankaranarayanan .
        14. Chen, X., Ábrahám, E., Sankaranarayanan, S.: ‘Flow*: an analyzer for non-linear hybrid systems’. Int. Conf. on Computer Aided Verification, 2013, pp. 258263.
        . Int. Conf. on Computer Aided Verification , 258 - 263
    15. 15)
      • S. Kong , S. Gao , W. Chen .
        15. Kong, S., Gao, S., Chen, W., et al: ‘dReach: δ-reachability analysis for hybrid systems’. Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2015, pp. 200205.
        . Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems , 200 - 205
    16. 16)
      • S. Gao , S. Kong , W. Chen .
        16. Gao, S., Kong, S., Chen, W., et al: ‘Delta-complete analysis for bounded reachability of hybrid systems’, arXiv preprint arXiv:1404.7171, 2014.
        .
    17. 17)
    18. 18)
      • P.S. Duggirala , S. Mitra , M. Viswanathan .
        18. Duggirala, P.S., Mitra, S., Viswanathan, M.: ‘Verification of annotated models from executions’. Proc. 11th ACM Int. Conf. on Embedded Software, 2013, p. 26.
        . Proc. 11th ACM Int. Conf. on Embedded Software , 26
    19. 19)
      • Z. Huang , S. Mitra .
        19. Huang, Z., Mitra, S.: ‘Computing bounded reach sets from sampled simulation traces’. Proc. of the 15th ACM Int. Conf. on Hybrid Systems: Computation and Control, 2012, pp. 291294.
        . Proc. of the 15th ACM Int. Conf. on Hybrid Systems: Computation and Control , 291 - 294
    20. 20)
      • Z. Huang , S. Mitra .
        20. Huang, Z., Mitra, S.: ‘Proofs from simulations and modular annotations’. Proc. 17th Int. Conf. on Hybrid Systems: Computation and Control, 2014, pp. 183192.
        . Proc. 17th Int. Conf. on Hybrid Systems: Computation and Control , 183 - 192
    21. 21)
      • C. Fan , S. Mitra .
        21. Fan, C., Mitra, S.: ‘Bounded verification with on-the-fly discrepancy computation’. Int. Symp. on Automated Technology for Verification and Analysis, 2015, pp. 446463.
        . Int. Symp. on Automated Technology for Verification and Analysis , 446 - 463
    22. 22)
      • S. Jiang .
        22. Jiang, S.: ‘Reachability analysis of linear hybrid automata by using counterexample fragment based abstraction refinement’. 2007 American Control Conf., 2007, pp. 41724177.
        . 2007 American Control Conf. , 4172 - 4177
    23. 23)
      • S. Jiang . (2006)
        23. Jiang, S.: ‘Abstraction based reachability analysis of concurrent linear hybrid automata’. GM Research Report ECI-293, Tech. Rep., 2006.
        .
    24. 24)
      • H. Ren , J. Huang , S. Jiang .
        24. Ren, H., Huang, J., Jiang, S., et al: ‘A new abstraction-refinement based verifier for modular linear hybrid automata and its implementation’. 2014 IEEE 11th Int. Conf. on Networking, Sensing and Control (ICNSC), 2014, pp. 3035.
        . 2014 IEEE 11th Int. Conf. on Networking, Sensing and Control (ICNSC) , 30 - 35
    25. 25)
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2017.0007
Loading

Related content

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