Generating and Analyzing Symbolic Traces of Simulink/Stateflow Models

  • Aditya Kanade
  • Rajeev Alur
  • Franjo Ivančić
  • S. Ramesh
  • Sriram Sankaranarayanan
  • K. C. Shashidhar
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


We present a methodology and a toolkit for improving simulation coverage of Simulink/Stateflow models of hybrid systems using symbolic analysis of simulation traces. We propose a novel instrumentation scheme that allows the simulation engine of Simulink/Stateflow to output, along with the concrete simulation trace, the symbolic transformers needed for our analysis. Given a simulation trace, along with the symbolic transformers, our analysis computes a set of initial states that would lead to traces with the same sequence of discrete components at each step of the simulation. Such an analysis relies critically on the use of convex polyhedra to represent sets of states. However, the exponential complexity of the polyhedral operations implies that the performance of the analysis would degrade rapidly with the increasing size of the model and the simulation traces. We propose a new representation, called the bounded vertex representation, which allows us to perform under-approximate computations while fixing the complexity of the representation a priori. Using this representation we achieve a trade-off between the complexity of the symbolic computation and the quality of the under-approximation. We demonstrate the benefits of our approach over existing simulation and verification methods with case studies.


Simulation Step Convex Polyhedron Hybrid Automaton Simulation Time Step Simulation Trace 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
  2. 2.
    Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. ENTCS 109, 43–56 (2004)zbMATHGoogle Scholar
  3. 3.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Alur, R., Kanade, A., Ramesh, S., Shashidhar, K.C.: Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In: EMSOFT, pp. 89–98 (2008)Google Scholar
  5. 5.
    Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Bournez, O., Maler, O., Pnueli, A.: Orthogonal polyhedra: Representation and computation. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 46–60. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  7. 7.
    Clarisó, R., Cortadella, J.: The octahedron abstract domain. Science of Computer Programming 64(1), 115–139 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Cleaveland, R., Smolka, S.A., Sims, S.: An instrumentation-based approach to controller model validation. In: Broy, M., Krüger, I.H., Meisinger, M. (eds.) ASWSD 2006. LNCS, vol. 4922, pp. 84–97. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  9. 9.
    Cousot, P., Cousot, R.: Static determination of dynamic properties of programs. In: Proc. of the Second International Symp. on Programming, pp. 106–130 (1976)Google Scholar
  10. 10.
    Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL, pp. 84–96 (1978)Google Scholar
  11. 11.
    Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  13. 13.
    Frehse, G.: PHAVer: Algorithmic verification of hybrid systems past HyTech. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 258–273. Springer, Heidelberg (2005)Google Scholar
  14. 14.
    Gadkari, A.A., Yeolekar, A., Suresh, J., Ramesh, S., Mohalik, S., Shashidhar, K.C.: AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 204–208. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. 15.
    Girard, A.: Reachability of uncertain linear systems using zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  16. 16.
    Girard, A., Guernic, C.L.: Zonotope/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215–228. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Girard, A., Pappas, G.J.: Verification using simulation. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 272–286. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    GLPK (GNU Linear Programming Kit),
  19. 19.
    Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: PLDI, pp. 213–223 (2005)Google Scholar
  20. 20.
    Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. Form. Meth. in Sys. Design 11(2), 157–185 (1997)CrossRefGoogle Scholar
  21. 21.
    Henzinger, T.A., Ho, P.: HyTech: The Cornell hybrid technology tool. In: Antsaklis, P.J., Kohn, W., Nerode, A., Sastry, S.S. (eds.) HS 1994. LNCS, vol. 999, pp. 265–293. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  22. 22.
    Agung Julius, A., Fainekos, G.E., Anand, M., Lee, I., Pappas, G.J.: Robust test generation and coverage for hybrid systems. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 329–342. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Miné, A.: The octagon abstract domain. In: WCRE, p. 310 (2001)Google Scholar
  24. 24.
    Implementation of Qhull,
  25. 25.
    Reactis, Reactive Systems, Inc.,
  26. 26.
    Sankaranarayanan, S., Dang, T., Ivancic, F.: Symbolic model checking of hybrid systems using template polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  27. 27.
    Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Scalable analysis of linear systems using mathematical programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 25–41. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  28. 28.
    Simulink Design Verifier, The Mathworks, Inc.,
  29. 29.
    Sen, K., Marinov, D., Agha, G.: CUTE: a concolic unit testing engine for C. In: FSE, pp. 263–272 (2005)Google Scholar
  30. 30.
    Silva, B.I., Richeson, K., Krogh, B.H., Chutinan, A.: Modeling and verifying hybrid dynamic systems using CheckMate. In: ADPM (2000)Google Scholar
  31. 31.
    Simulink Reference, The Mathworks, Inc.,
  32. 32.
  33. 33.
    Stursberg, O., Krogh, B.H.: Efficient representation and computation of reachable sets for hybrid systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 482–497. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  34. 34.
    Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embedded Comput. Syst. 4(4), 779–818 (2005)CrossRefGoogle Scholar
  35. 35.
    T-VEC Tester, T-VEC Technologies, Inc.,

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Aditya Kanade
    • 1
  • Rajeev Alur
    • 1
  • Franjo Ivančić
    • 2
  • S. Ramesh
    • 3
  • Sriram Sankaranarayanan
    • 2
  • K. C. Shashidhar
    • 3
  1. 1.University of PennsylvaniaUSA
  2. 2.NEC Laboratories AmericaUSA
  3. 3.GM India Science LabIndia

Personalised recommendations