Your browser does not support JavaScript!
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

Simulink/Stateflow is a popular commercial model-based development tool for many industrial domains. For safety and security concerns, verification and testing must be performed on the Simulink/Stateflow designs and the generated code. The authors present a test generation approach for Simulink/Stateflow by its reduction to reachability in a hybrid automaton, with its locations representing the computations of the Simulink/Stateflow model, and edges representing the computation-succession. A novel reachability resolution method is presented based on the refinement of the hybrid automaton such that the reachability is reduced to the reachability in the underlying graph (without the dynamics), whenever the refinement step terminates. The approach yields a technique that is effective in terms of achieving test coverage and efficient in terms of test generation time whenever the computation of each time step can be analytically solved for an arbitrary number of repetition. The approach is also applied on defect-detection and requirements-satisfaction, and illustrated through application to a bounded counter and a cyberphysical system of a thermal control unit.

References

    1. 1)
    2. 2)
      • 10. Raskin, J.-F.: ‘Reachability problems for hybrid automata’. Reachability Problems, 2011 (LNCS, 6945), pp. 2830.
    3. 3)
      • 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.
    4. 4)
      • 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.
    5. 5)
      • 22. Jiang, S.: ‘Reachability analysis of linear hybrid automata by using counterexample fragment based abstraction refinement’. 2007 American Control Conf., 2007, pp. 41724177.
    6. 6)
      • 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.
    7. 7)
      • 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.
    8. 8)
      • 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.
    9. 9)
    10. 10)
      • 16. Gao, S., Kong, S., Chen, W., et al: ‘Delta-complete analysis for bounded reachability of hybrid systems’, arXiv preprint arXiv:1404.7171, 2014.
    11. 11)
      • 23. Jiang, S.: ‘Abstraction based reachability analysis of concurrent linear hybrid automata’. GM Research Report ECI-293, Tech. Rep., 2006.
    12. 12)
      • 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.
    13. 13)
      • 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.
    14. 14)
      • 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.
    15. 15)
      • 20. Huang, Z., Mitra, S.: ‘Proofs from simulations and modular annotations’. Proc. 17th Int. Conf. on Hybrid Systems: Computation and Control, 2014, pp. 183192.
    16. 16)
      • 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.
    17. 17)
      • 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.
    18. 18)
      • 9. Alur, R.: ‘Formal verification of hybrid systems’. 2011 Proc. Int. Conf. on Embedded Software (EMSOFT), October 2011, pp. 273278.
    19. 19)
    20. 20)
    21. 21)
      • 1. Simulink/Stateflow, ‘https://www.mathworks.com/products/simulink.html’, [accessed: 23/02/2017].
    22. 22)
      • 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.
    23. 23)
    24. 24)
    25. 25)
      • 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.
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