Symbolic analysis for improving simulation coverage of Simulink/Stateflow models

ABSTRACT

Aimed at verifying safety properties and improving simulation coverage for hybrid systems models of embedded control software, we propose a technique that combines numerical simulation and symbolic methods for computing state-sets. We consider systems with linear dynamics described in the commercial modeling tool Simulink/Stateflow. Given an initial state x, and a discrete-time simulation trajectory, our method computes a set of initial states that are guaranteed to be equivalent to x, where two initial states are considered to be equivalent if the resulting simulation trajectories contain the same discrete components at each step of the simulation. We illustrate the benefits of our method on two case studies. One case study is a benchmark proposed in the literature for hybrid systems verification and another is a Simulink demo model from Mathworks.

REFERENCES

• 1: Simulink demos: http://www.mathworks.com/products/simulink/demos.html.
• 2: Simulink models of hybrid systems benchmarks http://www.cse.unsw.edu.au/~ansgar/benchmark/.
• 3: A. Agrawal, G. Simon, and G. Karsai. Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. ENTCS, 109:43--56, 2004.
• 4: R. Alur , C. Courcoubetis , N. Halbwachs , T. A. Henzinger , P.-H. Ho , X. Nicollin , A. Olivero , J. Sifakis , S. Yovine, The algorithmic analysis of hybrid systems, Theoretical Computer Science, v.138 n.1, p.3-34, Feb. 6, 1995 [doi>10.1016/0304-3975(94)00202-T]
• 5: Rajeev Alur , Thao Dang , Franjo Ivančić, Predicate abstraction for reachability analysis of hybrid systems, ACM Transactions on Embedded Computing Systems (TECS), v.5 n.1, p.152-199, February 2006 [doi>10.1145/1132357.1132363]
• 6: Roberto Bagnara , Patricia M. Hill , Enea Zaffanella, The Parma Polyhedra Library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems, Science of Computer Programming, v.72 n.1-2, p.3-21, June, 2008 [doi>10.1016/j.scico.2007.08.001]
• 7: C. Banphawatthanarak, B.H. Krogh, and K. Butts. Symbolic verification of executable control specifications. In Intl. Symp. on Computer Aided Control System Design, pages 581--586. IEEE, 1999.
• 8: BEACON Tester, Applied Dynamics International, http://www.adi.com/products_be_bss_te.htm.
• 9: Alongkrit Chutinan , Bruce H. Krogh, Verification of Polyhedral-Invariant Hybrid Automata Using Polygonal Flow Pipe Approximations, Proceedings of the Second International Workshop on Hybrid Systems: Computation and Control, p.76-90, March 29-31, 1999
• 10: E.M. Clarke, A. Fehnker, Z. Han, B.H. Krogh, J. Ouaknine, O. Stursberg, and M. Theobald. Abstraction and counterexample-guided abstraction refinement in model checking of hybrid systems. Intl. Journ. on Foundations of Computer Science, 14(4):583--604, 2003.
• 11: A. Donzé and O. Maler. Systematic simulation using sensitivity analysis. In HSCC, LNCS 4416, pages 174--189. Springer, 2007.
• 12: A. Fehnker and F. Ivancic. Benchmarks for hybrid systems verification. In HSCC, LNCS 2993, pages 326--341. Springer, 2004.
• 13: G. Frehse. Phaver: Algorithmic verification of hybrid systems past HyTech. In HSCC, LNCS 3414, pages 258--273. Springer, 2005.
• 14: Ambar A. Gadkari , Anand Yeolekar , J. Suresh , S. Ramesh , Swarup Mohalik , K. C. Shashidhar, AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control Systems, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_19]
• 15: A. Girard and G.J. Pappas. Approximation metrics for discrete and continuous systems. IEEE Trans. on Automatic Control, 52(5):782--798, 2007.
• 16: A. Girard and G.J. Pappas. Verification using simulation. In HSCC, LNCS 3927, pages 272--286. Springer, 2006.
• 17: Patrice Godefroid , Nils Klarlund , Koushik Sen, DART: directed automated random testing, Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, June 12-15, 2005, Chicago, IL, USA
• 18: N. Halbwachs, Y. Proy, and P. Raymond. Verification of linear hybrid systems by means of convex approximations. In SAS, LNCS 864, pages 223--237. Springer, 1994.
• 19: Grégoire Hamon, A denotational semantics for stateflow, Proceedings of the 5th ACM international conference on Embedded software, September 18-22, 2005, Jersey City, NJ, USA [doi>10.1145/1086228.1086260]
• 20: Grégoire Hamon , John Rushby, An operational semantics for Stateflow, International Journal on Software Tools for Technology Transfer (STTT), v.9 n.5, p.447-456, October 2007 [doi>10.1007/s10009-007-0049-7]
• 21: David Harel, Statecharts: A visual formalism for complex systems, Science of Computer Programming, v.8 n.3, p.231-274, June 1, 1987 [doi>10.1016/0167-6423(87)90035-9]
• 22: T.A. Henzinger, P. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. STTT, 1, 1997.
• 23: A.A. Julius, G.E. Fainekos, M. Anand, I. Lee, and G.J. Pappas. Robust test generation and coverage for hybrid systems. In HSCC, LNCS 4416, pages 329--342. Springer, 2007.
• 24: Alexander B. Kurzhanski , Pravin Varaiya, Ellipsoidal Techniques for Reachability Analysis, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, p.202-214, March 23-25, 2000
• 25: Edward A. Lee, What's Ahead for Embedded Software?, Computer, v.33 n.9, p.18-26, September 2000
• 26: Ian Mitchell , Claire Tomlin, Level Set Methods for Computation in Hybrid Systems, Proceedings of the Third International Workshop on Hybrid Systems: Computation and Control, p.310-323, March 23-25, 2000
• 27: T. Nahhal and T. Dang. Coverage for continuous and hybrid systems. In CAV, LNCS 4590, pages 449--462. Springer, 2007.
• 28: Reactis, Reactive Systems, Inc., http://www.reactive-systems.com.
• 29: S. Sankaranarayanan, T. Dang, and F. Ivancic. Symbolic model checking of hybrid systems using template polyhedra. In TACAS, LNCS 4963, pages 188--202. Springer, 2008.
• 30: S. Sastry, J. Sztipanovits, R. Bajcsy, and H. Gill. Modeling and design of embedded software. Proc. of the IEEE, 91(1), 2003.
• 31: Manoranjan Satpathy , Anand Yeolekar , S. Ramesh, Randomized directed testing (REDIRECT) for Simulink/Stateflow models, Proceedings of the 7th ACM international conference on Embedded software, October 19-24, 2008, Atlanta, GA, USA [doi>10.1145/1450058.1450088]
• 32: Simulink Design Verifier, The Mathworks, Inc., http://www.mathworks.com/products/sldesignverifier.
• 33: Koushik Sen , Darko Marinov , Gul Agha, CUTE: a concolic unit testing engine for C, Proceedings of the 10th European software engineering conference held jointly with 13th ACM SIGSOFT international symposium on Foundations of software engineering, September 05-09, 2005, Lisbon, Portugal
• 34: Safety Test Builder, TNI-Software., http://www.tni-software.com/en/produits/safetytestbuilder.
• 35: Ashish Tiwari, Abstractions for hybrid systems, Formal Methods in System Design, v.32 n.1, p.57-83, February 2008 [doi>10.1007/s10703-007-0044-3]
• 36: A. Tiwari. Formal semantics and analysis methods for Simulink Stateflow models. Technical report, SRI International, 2002.
• 37: Stavros Tripakis , Christos Sofronis , Paul Caspi , Adrian Curic, Translating discrete-time simulink to lustre, ACM Transactions on Embedded Computing Systems (TECS), v.4 n.4, p.779-818, November 2005 [doi>10.1145/1113830.1113834]
• 38: T-VEC Tester, T-VEC Technologies, Inc., http://www.t-vec.com/solutions/simulink.php.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

Additional Classification:
  I. Computing Methodologies
  I.6 SIMULATION AND MODELING
      I.6.4 Model Validation and Analysis

General Terms:
Design, Experimentation, Measurement, Verification

Keywords:
Simulink, Stateflow, coverage, hybrid systems, simulations