This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)
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)
-
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. 3918–3925.
-
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. 462–467.
-
4)
-
5)
-
57. Groce, A.D.: ‘Error explanation and fault localization with distance metrics’. PhD. dissertation, NASA, 2005.
-
6)
-
62. Li, M., Kumar, R.: ‘Robustness of Simulink/Stateflow model against implementation imperfections’, IFAC-PapersOnLine, 2015, 48, (27), pp. 274–279 (doi: 10.1016/j.ifacol.2015.11.187).
-
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. 254–257.
-
8)
-
35. Dang, T., Nahhal, T.: ‘Coverage-guided test generation for continuous and hybrid systems’, Formal Methods Syst. Design, 2009, 34, (2), pp. 183–213 (doi: 10.1007/s10703-009-0066-0).
-
9)
-
16. Tripakis, S., Sofronis, C., Caspi, P., et al: ‘Translating discrete-time simulink to lustre’, ACM Trans. Embed. Comput. Syst., 2005, 4, (4), pp. 779–818 (doi: 10.1145/1113830.1113834).
-
10)
-
54. Beer, I., Ben-David, S., Eisner, C., et al: ‘Efficient detection of vacuity in temporal model checking’, Formal Methods Syst. Design, 2001, 18, (2), pp. 141–163 (doi: 10.1023/A:1008779610539).
-
11)
-
56. Dodoo, N., Donovan, A., Lin, L., et al: ‘Selecting predicates for implications in program analysis’, 2002.
-
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)
-
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. 229–237.
-
14)
-
46. Niu, F.: ‘Learning-based software testing using symbolic constraint solving methods’. (KTH Royal Institute of Technology, 2011).
-
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. 585–588.
-
16)
-
51. Kesten, Y., Manna, Z., McGuire, H., et al: ‘A decision algorithm for full propositional temporal logic’, Comput. Aided Verif., 1993, 697, pp. 97–109.
-
17)
-
30. Binh, N.T., Tung, K.T.: ‘A novel fitness function of metaheuristic algorithms for test data generation for Simulink models based on mutation analysis’, J. Syst. Softw., 2016, 120, pp. 17–30 (doi: 10.1016/j.jss.2016.07.001).
-
18)
-
60. Zeller, A.: ‘Isolating cause-effect chains from computer programs’. Proc. 10th ACM SIGSOFT Symp. on Foundations of Software Engineering, 2002, pp. 1–10.
-
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. 224–229.
-
20)
-
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. 217–226.
-
22)
-
2. Li, M., Kumar, R.: ‘Recursive modeling of stateflow as input/output-extended automaton’, IEEE Trans. Autom. Sci. Eng., 2014, 11, (4), pp. 1229–1239 (doi: 10.1109/TASE.2013.2272535).
-
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 (, 6286), pp. 208–227.
-
24)
-
40. Bhatt, D., Madl, G., Schloegel, K.: ‘Towards scalable veri cation of commercial avionics software’. Proc. AIAA Infotech@Aerospace Conf., April 2010.
-
25)
-
49. Gastin, P., Oddoux, D.: ‘Fast ltl to Büchi automata translation’, Comput. Aided Verif., 2001, 2102, pp. 53–65.
-
26)
-
55. Cleve, H., Zeller, A.: ‘Locating causes of program failures’. Proc. 27th Int. Conf. on Software Engineering, 2005, pp. 342–351.
-
27)
-
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. 30–39.
-
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)
-
47. Visser, W., Păsăreanu, C.S., Khurshid, S.: ‘Test input generation with java pathfinder’, SIGSOFT Softw. Eng. Notes, 2004, 29, (4), pp. 97–107. .
-
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. 53–62.
-
32)
-
33)
-
52. Vardi, M.Y., Wolper, P.: ‘Reasoning about infinite computations’, Inf. Comput., 1994, 115, pp. 1–37 (doi: 10.1006/inco.1994.1092).
-
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)
-
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. 3–18.
-
37)
-
17. Miller, S.P., Whalen, M.W., Cofer, D.D.: ‘Software model checking takes off’, Commun. ACM, 2010, 53, (2), pp. 58–64 (doi: 10.1145/1646353.1646372).
-
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. 259–268.
-
39)
-
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. 308–311.
-
41)
-
58. Pytlik, B., Renieris, M., Krishnamurthi, S., et al: ‘Automated fault localization using potential invariants’. , 2003.
-
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. 4086–4095.
-
43)
-
44)
-
45)
-
46)
-
45. Groce, A., Havelund, K., Holzmann, G., et al: ‘Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning’, Ann. Math. Artif. Intell., 2014, 70, (4), pp. 315–349 (doi: 10.1007/s10472-014-9408-8).
-
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. 595–606.
-
48)
-
48. Biere, A., Cimatti, A., Clarke, E.M., et al: ‘Bounded model checking’, Adv. Comput., 2003, 58, pp. 117–148 (doi: 10.1016/S0065-2458(03)58003-2).
-
49)
-
50)
-
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. 261–270.
-
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)
-
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. 1–6.
-
55)
-
34. Donzé, A.: ‘Breach, a toolbox for verification and parameter synthesis of hybrid systems’. Int. Conf. on Computer Aided Verification, 2010, pp. 167–170.
-
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, . GECCO'11, New York, NY, USA, 2011, pp. 1851–1858.
-
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)
-
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. 5127–5132.
-
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. 179–180.
-
60)
-
5. Zhou, C., Kumar, R.: ‘Semantic translation of Simulink diagrams to input/output extended finite automata’, Discrete Event Dynamic Systems, 2010, 22, (2), pp. 223–247 (doi: 10.1007/s10626-010-0096-1).
-
61)
-
53. Emerson, E.A.: ‘Temporal and modal logic’, in J. van Leeuwen (Ed.) ‘Handbook of theoretical computer science’ (Elsevier, 1995), pp. 995–1072.
-
62)
http://iet.metastore.ingenta.com/content/journals/10.1049/iet-cps.2016.0024
Related content
content/journals/10.1049/iet-cps.2016.0024
pub_keyword,iet_inspecKeyword,pub_concept
6
6