Skip to main content
SpringerLink
Log in

Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines

  • Conference paper
Book cover NASA Formal Methods (NFM 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7226))

Included in the following conference series:

Abstract

The paper introduces a technique to symbolically execute hierarchically composed models based on communicating state machines. The technique is modular and starts with non-composite models, which are symbolically executed. The results of the execution, symbolic execution trees, are then composed according to the communication topology. The composite symbolic execution trees may be composed further reflecting hierarchical structure of the analyzed model. The technique supports reuse, meaning that already generated symbolic execution trees, composite or not, are used any time they are required in the composition. For illustration, the technique is applied to analyze UML-RT models and the paper shows several analyses options such as reachability checking or test case generation. The presentation of the technique is formal, but we also report on the implementation and we present some experimental results.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. IBM Rational Rhapsody Architect, Version 7.5.5, http://www-01.ibm.com/software/rational/products/rhapsody/swarchitect/

  2. IBM Rational Software Architect, RealTime Edition, Version 7.5.5, http://publib.boulder.ibm.com/infocenter/rsarthlp/v7r5m1/index.jsp

  3. Scade Suite, http://www.esterel-technologies.com/products/scade-suite/

  4. Unified Modeling Language (UML 2.0) Superstructure, http://www.uml.org/

  5. Alur, R., Kanade, A., Ramesh, S., Shashidhar, K.C.: Symbolic analysis for improving simulation coverage of Simulink/Stateflow models. In: EMSOFT 2008 (2008)

    Google Scholar 

  6. Anand, S., Pǎsǎreanu, C., Visser, W.: Symbolic execution with abstraction. Journ. on Soft. Tools for Techn. Transfer 11(1), 53–67 (2009)

    Article  Google Scholar 

  7. Anand, S., Godefroid, P., Tillmann, N.: Demand-Driven Compositional Symbolic Execution. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 367–381. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  8. Balser, M., Bäumler, S., Knapp, A., Reif, W., Thums, A.: Interactive Verification of UML State Machines. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 434–448. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  9. Balser, M., Duelli, C., Reif, W., Schellhorn, G.: Verifying concurrent systems with symbolic execution. Journal of Logic and Computation 12(4), 549 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  10. von der Beeck, M.: A Formal Semantics of UML-RT. In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 768–782. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  11. Burmester, S., Giese, H., Hirsch, M., Schilling, D.: Incremental design and formal verification with UML/RT in the FUJABA real-time tool suite. In: SVERTS 2004 (part of UML 2004) (2004)

    Google Scholar 

  12. Dillon, L.: Verifying General Safety Properties of Ada Tasking Programs. IEEE Trans. on Soft. Eng. 16 (1990)

    Google Scholar 

  13. Gaston, C., Aiguier, M., Bahrami, D., Lapitre, A.: Symbolic execution techniques extended to systems. In: ICSEA 2009 (2009)

    Google Scholar 

  14. Godefroid, P.: Compositional dynamic test generation. In: POPL 2007 (2007)

    Google Scholar 

  15. Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. SIGPLAN Notices 40(6), 213–223 (2005)

    Article  Google Scholar 

  16. Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: NDSS 2008 (2008)

    Google Scholar 

  17. King, J.: Symbolic execution and program testing. Communications of the ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  18. Lee, N.H., Cha, S.D.: Generating test sequence using symbolic execution for event-driven real-time systems. Microproc. and Microsys. 27, 523–531 (2003)

    Article  Google Scholar 

  19. Pǎsǎreanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. J. on Software Tools for Technology Transfer 11 (2009)

    Google Scholar 

  20. Rapin, N.: Symbolic Execution Based Model Checking of Open Systems with Unbounded Variables. In: Dubois, C. (ed.) TAP 2009. LNCS, vol. 5668, pp. 137–152. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  21. Selic, B.: Using UML for Modeling Complex Real-Time Systems. In: Müller, F., Bestavros, A. (eds.) LCTES 1998. LNCS, vol. 1474, pp. 250–260. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  22. Sperschneider, V., Antoniou, G.: Logic: a foundation for computer science. Addison-Wesley (1991)

    Google Scholar 

  23. Thums, A., Schellhorn, G., Ortmeier, F., Reif, W.: Interactive Verification of Statecharts. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 355–373. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  24. Tomb, A., Brat, G., Visser, W.: Variably interprocedural program analysis for runtime error detection. In: ISSTA 2007 (2007)

    Google Scholar 

  25. Zurowska, K., Dingel, J.: SAUML: a Tool for Symbolic Execution of UML-RT Models. In: ASE 2011 - Tool Demonstrations (2011) (to appear)

    Google Scholar 

  26. Zurowska, K., Dingel, J.: Symbolic execution of UML-RT State Machines. In: SAC - Software Verification and Testing 2012 (to appear, 2012)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Computing, Queen’s University, Kingston, ON, Canada

    Karolina Zurowska & Juergen Dingel

Authors
  1. Karolina Zurowska
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Juergen Dingel
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NASA Langley Research Center, MS 130, 23681, Hampton, VA, USA

    Alwyn E. Goodloe  & Suzette Person  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Zurowska, K., Dingel, J. (2012). Symbolic Execution of Communicating and Hierarchically Composed UML-RT State Machines. In: Goodloe, A.E., Person, S. (eds) NASA Formal Methods. NFM 2012. Lecture Notes in Computer Science, vol 7226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-28891-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-28891-3_6

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-28890-6

  • Online ISBN: 978-3-642-28891-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation