Skip to main content
SpringerLink
Log in
Book cover

International Conference on Formal Engineering Methods

ICFEM 2002: Formal Methods and Software Engineering pp 435–446Cite as

Slicing Hierarchical Automata for Model Checking UML Statecharts

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2495))

Abstract

Hierarchical Automata has been widely used in modeling dynamic aspects of reactive software, such as in UML Statecharts. At the same time, model checking is an automatic technique to ensure the correctness of software models, where state space explosion is the main obstacle to applying this technique in large scale applications. The paper presents a method for slicing hierarchical automata with respect to properties to be verified. The considered formalism is Extended Hierarchical Automata (EHA), in which a set of dependence relations is specified after analyzing characteristics such as hierarchy, concurrency and synchronization. We present the algorithm of slicing EHA based on the slicing criterion in terms of states and transitions. The algorithm can remove the hierarchies and concurrent states which are irrelevant to the property, and reduce the state space efficiently in model checking UML Statecharts.

Supported by National Natural Science Foundation of China Grants No. 69973051 and No. 90104007, 863 Hi-Tech Programme of China Grant No. 2001AA113202 and Huo Ying Dong Education Foundation Grant No. 71064.

This is a preview of subscription content, 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   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D. Harel. Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming. Elsevier, 8(3): 231–274, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  2. OMG Document ad/97-08-04. Rational Software et.al., 1997.

    Google Scholar 

  3. J. Lilius and I.P. Paltor. vUML: A Tool for Verifying UML Models. TUCS Technical Report No 272, 1999.

    Google Scholar 

  4. E. Mikk, Y. Lakhnech, M. Siegel, and G.J. Holzmann. Implementing Statecharts in PROMELA/SPIN. In Proceedings of Workshop on Industrial-Strength Formal Specification Techniques (WIFT’ 98), 1998.

    Google Scholar 

  5. S. Gnesi and D. Latella. Model Checking UML Statecharts Diagrams Using JACK. In Proceedings of the 4th IEEE International Symposium on High-Assurance Systems Engineering, 1999.

    Google Scholar 

  6. W. Dong, J. Wang, X. Qi and Z.C. Qi. Model Checking UML Statecharts. In Proceedings of the Eighth Asia-Pacific Software Engineering Conference (APSEC 2001). IEEE Computer Society Press, December 2001.

    Google Scholar 

  7. M.P.E. Heimdahl and M. Whalen. Reduction and Slicing of Hierarchical State Machines. In Proceedings of the Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering, September 1997.

    Google Scholar 

  8. M.B. Dwyer and J. Hatcliff. Slicing Software for Model Construction. In ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, 1999.

    Google Scholar 

  9. Lynette I. Millett and Tim Teitelbaum. Slicing Promela and its Applications to Model Checking, simulation, and protocol understanding. In Proceedings of the SPIN 98 Workshop in Paris, France, November 1998.

    Google Scholar 

  10. John Hatcliff, James Corbett, Matthew Dwyer, Stefan Sokolowski, and Hongjun Zheng. A Formal Study of Slicing for Multi-Threaded Programs with JVM Concurrency Primitives. In Proceedings of the International Symposium on Static Analysis (SAS’99), September 1999.

    Google Scholar 

  11. M. Weiser. Program Slicing. IEEE Trans. Softw. Eng, SE(10), 4, 1984.

    Google Scholar 

  12. J. Cheng. Slicing Concurrent Programs-A Graph-Theoretical Approach. In Proceedings of the First International Workshop on Automated Algorithmic Debugging, LNCS, Vol. 749. Springer-Verlag, May 1993.

    Chapter  Google Scholar 

  13. A. Puneli. The Temporal Semantics of Concurrent Programs. Theoretical Computer Science 13: 45–60, 1981.

    Article  MathSciNet  Google Scholar 

  14. Edmund M. Clarke, Orna Grumberg and Doron Peled. Model Checking, MIT Press, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. National Laboratory for Parallel and Distributed Processing, P.R. China

    Wang Ji, Dong Wei & Qi Zhi-Chang

Authors
  1. Wang Ji
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dong Wei
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Qi Zhi-Chang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. International Institute for Software Technology, United Nations University, Casa Silva Mendes, Est. do Engenheiro Trigo No. 4, P.O. Box 3058, Macao

    Chris George

  2. School of Computer Engineering and Science, Shanghai University, 149 Yanchang Road, Shanghai, 200072, P.R. China

    Huaikou Miao

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ji, W., Wei, D., Zhi-Chang, Q. (2002). Slicing Hierarchical Automata for Model Checking UML Statecharts. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_45

Download citation

  • DOI: https://doi.org/10.1007/3-540-36103-0_45

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00029-7

  • Online ISBN: 978-3-540-36103-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation