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

access icon openaccess Automated test generation and error localisation for Simulink/Stateflow modelled systems using extended automata

Model-based development frameworks for cyber-physical systems (CPSs) such as Simulink and Stateflow are popular for many applications. For safety and security concerns, verification and testing/validation must be performed on the model-based CPS designs. In this study, the authors present an automatic test generation approach for model-based CPS designs in Simulink/Stateflow based on its translation to input/output extended finite automata (I/O-EFA) developed in the authors’ prior works. The test generation problem requires identifying the executable paths of the I/O-EFA model and also generating a test input for those paths. To execute a path, a certain sequence of other paths must be executed first, which they automatically identify. The approach is implemented by applying two different techniques, model checking and constraint solving. Both test generation implementations are validated by a case study. The results show that both implementations can generate test cases, while the implementation based on constraint solving is in general faster. The approach is further extended to requirements-based test generation. These tests are then used for validation purposes, and the failed versus passed tests are used to localise the fault to plausible Simulink/Stateflow blocks using the notion of fault-seed used in their earlier work. The approaches are applied on a bounded counter and a thermal control of a house as two different case studies.

References

    1. 1)
      • 8. ‘Reactis’, Available at http://www.reactive-systems.com/.
    2. 2)
      • 37. Zutshi, A., Sankaranarayanan, S., Deshmukh, J.V., et al: ‘A trajectory splicing approach to concretizing counterexamples for hybrid systems’. 52nd IEEE Conf. on Decision and Control, 2013, pp. 39183925.
    3. 3)
      • 4. 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.
    4. 4)
      • 22. ‘Yices’, Available at: http://yices.csl.sri.com/.
    5. 5)
      • 57. Groce, A.D.: ‘Error explanation and fault localization with distance metrics’. PhD. dissertation, NASA, 2005.
    6. 6)
    7. 7)
      • 33. Annpureddy, Y., Liu, C., Fainekos, G., et al: ‘S-taliro: a tool for temporal logic falsification for hybrid systems’. Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, 2011, pp. 254257.
    8. 8)
    9. 9)
    10. 10)
    11. 11)
      • 56. Dodoo, N., Donovan, A., Lin, L., et al: ‘Selecting predicates for implications in program analysis’, 2002.
    12. 12)
      • 7. 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.
    13. 13)
      • 14. Marre, B., Arnould, A.: ‘Test sequences generation from lustre descriptions: Gatel’. The Fifteenth IEEE Int. Conf. on Automated Software Engineering, 2000. Proc. ASE 2000, 2000, pp. 229237.
    14. 14)
      • 46. Niu, F.: ‘Learning-based software testing using symbolic constraint solving methods’. Computer Science and Communication (KTH Royal Institute of Technology, 2011).
    15. 15)
      • 41. Matinnejad, R., Nejati, S., Briand, L.C., et al: ‘Simcotest: a test suite generation tool for simulink/stateflow controllers’. Proc. 38th Int. Conf. on Software Engineering Companion, 2016, pp. 585588.
    16. 16)
      • 51. Kesten, Y., Manna, Z., McGuire, H., et al: ‘A decision algorithm for full propositional temporal logic’, Comput. Aided Verif., 1993, 697, pp. 97109.
    17. 17)
    18. 18)
      • 60. Zeller, A.: ‘Isolating cause-effect chains from computer programs’. Proc. 10th ACM SIGSOFT Symp. on Foundations of Software Engineering, 2002, pp. 110.
    19. 19)
      • 29. He, N., Rümmer, P., Kroening, D.: ‘Test-case generation for embedded Simulink via formal concept analysis’. Proc. 48th Design Automation Conf., ser. DAC'11, New York, NY, USA, 2011, pp. 224229.
    20. 20)
      • 26. ‘Matlab’, Available at: https://www.mathworks.com/products/matlab/.
    21. 21)
      • 9. Satpathy, M., Yeolekar, A., Ramesh, S.: ‘Randomized directed testing (redirect) for simulink/stateflow models’. ser. EMSOFT'08, New York, NY, USA, 2008, pp. 217226.
    22. 22)
    23. 23)
      • 28. Brillout, A., He, N., Mazzucchi, M., et al: ‘Mutation-based test case generation for Simulink models’. Formal Methods for Components and Objects, 2010 (LNCS, 6286), pp. 208227.
    24. 24)
      • 40. Bhatt, D., Madl, G., Schloegel, K.: ‘Towards scalable veri cation of commercial avionics software’. Proc. AIAA Infotech@Aerospace Conf., April 2010.
    25. 25)
      • 49. Gastin, P., Oddoux, D.: ‘Fast ltl to Büchi automata translation’, Comput. Aided Verif., 2001, 2102, pp. 5365.
    26. 26)
      • 55. Cleve, H., Zeller, A.: ‘Locating causes of program failures’. Proc. 27th Int. Conf. on Software Engineering, 2005, pp. 342351.
    27. 27)
      • 1. ‘Simulink’, Available at http://www.mathworks.com/products/simulink/.
    28. 28)
      • 59. Renieres, M., Reiss, S.P.: ‘Fault localization with nearest neighbor queries’. Proc. 18th IEEE Int. Conf. on Automated Software Engineering, 2003, 2003, pp. 3039.
    29. 29)
      • 42. Ebdelli, N., Ahmed, S.B.: ‘Simautogen tool: test vector generation from large scale Matlab/Simulink models’. Formal Techniques for Distributed Objects, Components, and Systems: 36th IFIP WG 6.1 Int. Conf., FORTE 2016, Held as Part of the 11th Int. Federated Conf. on Distributed Computing Techniques, DisCoTec 2016, Proc., Heraklion, Crete, Greece, 6–9 June 2016, vol. 9688, p. 267.
    30. 30)
      • 47. Visser, W., Păsăreanu, C.S., Khurshid, S.: ‘Test input generation with java pathfinder’, SIGSOFT Softw. Eng. Notes, 2004, 29, (4), pp. 97107. Available at: http://doi.acm.org/10.1145/1013886.1007526=0pt.
    31. 31)
      • 23. Gotlieb, A., Botella, B., Rueher, M.: ‘Automatic test data generation using constraint solving techniques’. ACM SIGSOFT Software Engineering Notes, 1998, vol. 23, no. 2, pp. 5362.
    32. 32)
      • 25. ‘Cplex’, Available at: https://www-01.ibm.com/software/commerce/optimization/cplex-optimizer/.
    33. 33)
    34. 34)
      • 36. Zutshi, A., Deshmukh, J.V., Sankaranarayanan, S., et al: ‘Multiple shooting, cegar-based falsification for hybrid systems’. Proc. of the 14th Int. Conf. on Embedded Software, 2014, p. 5.
    35. 35)
      • 39. ‘T-vec’, Available at: http://www.t-vec.com/.
    36. 36)
      • 50. Gerth, R., Peled, D., Vardi, M.Y., et al: ‘Simple on-the-fly automatic verification of linear temporal logic’. Proc. 15th IFIP WG6.1 Int. Symp. on Protocol Specification, Testing and Verification (PSTV95), June 1995, vol. 115, pp. 318.
    37. 37)
    38. 38)
      • 15. Scaife, N., Sofronis, C., Caspi, P., et al: ‘Defining and translating a ‘safe’ subset of Simulink/Stateflow into lustre’. EMSOFT'04: Proc. Fourth ACM Int. Conf. on Embedded Software, 2004, pp. 259268.
    39. 39)
      • 44. ‘Cvx’, Available at: http://cvxr.com/cvx/.
    40. 40)
      • 31. Peranandam, P., Raviram, S., Satpathy, M., et al: ‘An integrated test generation tool for enhanced coverage of Simulink/Stateflow models’. Design, Automation Test in Europe Conf. Exhibition (DATE), 2012, March 2012, pp. 308311.
    41. 41)
      • 58. Pytlik, B., Renieris, M., Krishnamurthi, S., et al: ‘Automated fault localization using potential invariants’. arXiv preprint cs/0310040, 2003.
    42. 42)
      • 32. Kapinski, J., Deshmukh, J., Jin, X., et al: ‘Simulation-guided approaches for verification of automotive powertrain control systems’. 2015 American Control Conf. (ACC), 2015, pp. 40864095.
    43. 43)
      • 43. ‘Nusmv’, Available at: http://nusmv.fbk.eu/.
    44. 44)
      • 18. ‘Prover’, Available at: http://www.prover.com/.
    45. 45)
      • 27. ‘Maple’, Available at: http://www.maplesoft.com/products/Maple/.
    46. 46)
    47. 47)
      • 38. Matinnejad, R., Nejati, S., Briand, L.C., et al: ‘Automated test suite generation for time-continuous simulink models’. Proc. 38th Int. Conf. on Software Engineering, 2016, pp. 595606.
    48. 48)
    49. 49)
      • 11. ‘Simulink Design Verifier’, Available at: http://www.mathworks.com/products/sldesignverifier/.
    50. 50)
      • 21. ‘dreal’, Available at: https://dreal.github.io/.
    51. 51)
      • 13. Hamon, G., de Moura, L., Rushby, J.: ‘Generating efficient test sets with a model checker’. Software Engineering and Formal Methods, 2004, 2004, pp. 261270.
    52. 52)
      • 12. Gadkari, A., Mohalik, S., Shashidhar, K., et al: ‘Automatic generation of test-cases using model checking for sl/sf models’. Fourth Int. Workshop on Model Driven Engineering, Verification and Validation, 2007.
    53. 53)
      • 19. ‘Z3’, Available at: https://github.com/Z3Prover/z3.
    54. 54)
      • 3. Li, M., Kumar, R.: ‘Stateflow to extended finite automata translation’. 35th Annual Computer Software and Applications Conf. Workshops (COMPSACW), 2011, July 2011, pp. 16.
    55. 55)
      • 34. Donzé, A.: ‘Breach, a toolbox for verification and parameter synthesis of hybrid systems’. Int. Conf. on Computer Aided Verification, 2010, pp. 167170.
    56. 56)
      • 10. Oh, J., Harman, M., Yoo, S.: ‘Transition coverage testing for Simulink/Stateflow models using messy genetic algorithms’. Proc. 13th Annual Conf. on Genetic and Evolutionary Computation, ser. GECCO'11, New York, NY, USA, 2011, pp. 18511858.
    57. 57)
      • 6. 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.
    58. 58)
      • 61. Zhou, C., Kumar, R., Jiang, S.: ‘A formal analysis approach of runtime data-log for embedded software-fault localization’. 2011 American Control Conf., June 2011, vol. 115, pp. 51275132.
    59. 59)
      • 24. Păsăreanu, C.S., Rungta, N.: ‘Symbolic pathfinder: symbolic execution of java bytecode’. Proc. of the IEEE/ACM Int. Conf. on Automated Software Engineering, 2010, pp. 179180.
    60. 60)
    61. 61)
      • 53. Emerson, E.A.: ‘Temporal and modal logic’, in J. van Leeuwen (Ed.) ‘Handbook of theoretical computer science’ (Elsevier, 1995), pp. 9951072.
    62. 62)
      • 20. ‘Kind2’, Available at: http://kind2-mc.github.io/kind2/.
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2016.0024
Loading

Related content

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