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

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

  • XML
    325.2783203125Kb
  • PDF
    633.1015625Kb
  • HTML
    421.78125Kb
Loading full text...

Full text loading...

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

References

    1. 1)
      • 1. ‘Simulink’, Available at http://www.mathworks.com/products/simulink/.
        .
    2. 2)
    3. 3)
      • M. Li , R. Kumar .
        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.
        . 35th Annual Computer Software and Applications Conf. Workshops (COMPSACW), 2011 , 1 - 6
    4. 4)
      • C. Zhou , R. Kumar .
        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.
        . Annual Int. Computer Software and Applications Conf. , 462 - 467
    5. 5)
    6. 6)
      • M. Li , R. Kumar .
        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.
        . Proc. Eighth IEEE Int. Conf. on Automation Science and Engineering (CASE 2013)
    7. 7)
      • M. Li , R. Kumar .
        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.
        . Proc. Eighth IEEE Int. Conf. on Automation Science and Engineering (CASE 2012)
    8. 8)
      • 8. ‘Reactis’, Available at http://www.reactive-systems.com/.
        .
    9. 9)
      • M. Satpathy , A. Yeolekar , S. Ramesh .
        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.
        . ser. EMSOFT'08 , 217 - 226
    10. 10)
      • J. Oh , M. Harman , S. Yoo .
        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.
        . Proc. 13th Annual Conf. on Genetic and Evolutionary Computation , 1851 - 1858
    11. 11)
      • 11. ‘Simulink Design Verifier’, Available at: http://www.mathworks.com/products/sldesignverifier/.
        .
    12. 12)
      • A. Gadkari , S. Mohalik , K. Shashidhar .
        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.
        . Fourth Int. Workshop on Model Driven Engineering, Verification and Validation
    13. 13)
      • G. Hamon , L. de Moura , J. Rushby .
        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.
        . Software Engineering and Formal Methods, 2004 , 261 - 270
    14. 14)
      • B. Marre , A. Arnould .
        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.
        . The Fifteenth IEEE Int. Conf. on Automated Software Engineering, 2000. Proc. ASE 2000 , 229 - 237
    15. 15)
      • N. Scaife , C. Sofronis , P. Caspi .
        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.
        . EMSOFT'04: Proc. Fourth ACM Int. Conf. on Embedded Software , 259 - 268
    16. 16)
    17. 17)
    18. 18)
      • 18. ‘Prover’, Available at: http://www.prover.com/.
        .
    19. 19)
      • 19. ‘Z3’, Available at: https://github.com/Z3Prover/z3.
        .
    20. 20)
      • 20. ‘Kind2’, Available at: http://kind2-mc.github.io/kind2/.
        .
    21. 21)
      • 21. ‘dreal’, Available at: https://dreal.github.io/.
        .
    22. 22)
      • 22. ‘Yices’, Available at: http://yices.csl.sri.com/.
        .
    23. 23)
      • A. Gotlieb , B. Botella , M. Rueher .
        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.
        . ACM SIGSOFT Software Engineering Notes , 2 , 53 - 62
    24. 24)
      • C.S. Păsăreanu , N. Rungta .
        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.
        . Proc. of the IEEE/ACM Int. Conf. on Automated Software Engineering , 179 - 180
    25. 25)
      • 25. ‘Cplex’, Available at: https://www-01.ibm.com/software/commerce/optimization/cplex-optimizer/.
        .
    26. 26)
      • 26. ‘Matlab’, Available at: https://www.mathworks.com/products/matlab/.
        .
    27. 27)
      • 27. ‘Maple’, Available at: http://www.maplesoft.com/products/Maple/.
        .
    28. 28)
      • A. Brillout , N. He , M. Mazzucchi .
        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.
        . Formal Methods for Components and Objects , 208 - 227
    29. 29)
      • N. He , P. Rümmer , D. Kroening .
        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.
        . Proc. 48th Design Automation Conf., ser. DAC'11 , 224 - 229
    30. 30)
    31. 31)
      • P. Peranandam , S. Raviram , M. Satpathy .
        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.
        . Design, Automation Test in Europe Conf. Exhibition (DATE), 2012 , 308 - 311
    32. 32)
      • J. Kapinski , J. Deshmukh , X. Jin .
        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.
        . 2015 American Control Conf. (ACC) , 4086 - 4095
    33. 33)
      • Y. Annpureddy , C. Liu , G. Fainekos .
        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.
        . Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems , 254 - 257
    34. 34)
      • A. Donzé .
        34. Donzé, A.: ‘Breach, a toolbox for verification and parameter synthesis of hybrid systems’. Int. Conf. on Computer Aided Verification, 2010, pp. 167170.
        . Int. Conf. on Computer Aided Verification , 167 - 170
    35. 35)
    36. 36)
      • A. Zutshi , J.V. Deshmukh , S. Sankaranarayanan .
        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.
        . Proc. of the 14th Int. Conf. on Embedded Software
    37. 37)
      • A. Zutshi , S. Sankaranarayanan , J.V. Deshmukh .
        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.
        . 52nd IEEE Conf. on Decision and Control , 3918 - 3925
    38. 38)
      • R. Matinnejad , S. Nejati , L.C. Briand .
        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.
        . Proc. 38th Int. Conf. on Software Engineering , 595 - 606
    39. 39)
      • 39. ‘T-vec’, Available at: http://www.t-vec.com/.
        .
    40. 40)
      • D. Bhatt , G. Madl , K. Schloegel .
        40. Bhatt, D., Madl, G., Schloegel, K.: ‘Towards scalable veri cation of commercial avionics software’. Proc. AIAA Infotech@Aerospace Conf., April 2010.
        . Proc. AIAA Infotech@Aerospace Conf.
    41. 41)
      • R. Matinnejad , S. Nejati , L.C. Briand .
        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.
        . Proc. 38th Int. Conf. on Software Engineering Companion , 585 - 588
    42. 42)
      • N. Ebdelli , S.B. Ahmed .
        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.
        . 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. , 267
    43. 43)
      • 43. ‘Nusmv’, Available at: http://nusmv.fbk.eu/.
        .
    44. 44)
      • 44. ‘Cvx’, Available at: http://cvxr.com/cvx/.
        .
    45. 45)
    46. 46)
      • F. Niu . (2011)
        46. Niu, F.: ‘Learning-based software testing using symbolic constraint solving methods’. Computer Science and Communication (KTH Royal Institute of Technology, 2011).
        .
    47. 47)
      • W. Visser , C.S. Păsăreanu , S. Khurshid .
        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.
        . SIGSOFT Softw. Eng. Notes , 4 , 97 - 107
    48. 48)
    49. 49)
      • P. Gastin , D. Oddoux .
        49. Gastin, P., Oddoux, D.: ‘Fast ltl to Büchi automata translation’, Comput. Aided Verif., 2001, 2102, pp. 5365.
        . Comput. Aided Verif. , 53 - 65
    50. 50)
      • R. Gerth , D. Peled , M.Y. Vardi .
        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.
        . Proc. 15th IFIP WG6.1 Int. Symp. on Protocol Specification, Testing and Verification (PSTV95) , 3 - 18
    51. 51)
      • Y. Kesten , Z. Manna , H. McGuire .
        51. Kesten, Y., Manna, Z., McGuire, H., et al: ‘A decision algorithm for full propositional temporal logic’, Comput. Aided Verif., 1993, 697, pp. 97109.
        . Comput. Aided Verif. , 97 - 109
    52. 52)
    53. 53)
      • E.A. Emerson . (1995)
        53. Emerson, E.A.: ‘Temporal and modal logic’, in J. van Leeuwen (Ed.) ‘Handbook of theoretical computer science’ (Elsevier, 1995), pp. 9951072.
        .
    54. 54)
    55. 55)
      • H. Cleve , A. Zeller .
        55. Cleve, H., Zeller, A.: ‘Locating causes of program failures’. Proc. 27th Int. Conf. on Software Engineering, 2005, pp. 342351.
        . Proc. 27th Int. Conf. on Software Engineering , 342 - 351
    56. 56)
      • N. Dodoo , A. Donovan , L. Lin .
        56. Dodoo, N., Donovan, A., Lin, L., et al: ‘Selecting predicates for implications in program analysis’, 2002.
        .
    57. 57)
      • A.D. Groce .
        57. Groce, A.D.: ‘Error explanation and fault localization with distance metrics’. PhD. dissertation, NASA, 2005.
        . PhD. dissertation
    58. 58)
      • B. Pytlik , M. Renieris , S. Krishnamurthi .
        58. Pytlik, B., Renieris, M., Krishnamurthi, S., et al: ‘Automated fault localization using potential invariants’. arXiv preprint cs/0310040, 2003.
        .
    59. 59)
      • M. Renieres , S.P. Reiss .
        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.
        . Proc. 18th IEEE Int. Conf. on Automated Software Engineering, 2003 , 30 - 39
    60. 60)
      • A. Zeller .
        60. Zeller, A.: ‘Isolating cause-effect chains from computer programs’. Proc. 10th ACM SIGSOFT Symp. on Foundations of Software Engineering, 2002, pp. 110.
        . Proc. 10th ACM SIGSOFT Symp. on Foundations of Software Engineering , 1 - 10
    61. 61)
      • C. Zhou , R. Kumar , S. Jiang .
        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.
        . 2011 American Control Conf. , 5127 - 5132
    62. 62)
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