Skip to main content
SpringerLink
Log in

Rewrite Rules and Operational Semantics for Model Checking UML Statecharts

  • Conference paper
  • First Online:
≪UML≫ 2000 — The Unified Modeling Language (UML 2000)

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

Included in the following conference series:

Abstract

Model checking of UML statecharts is the main concern of this paper. To model check it, however, its description has to be translated into the input language of the model checker SMV. For the purpose of translating UML statecharts as closely as possible into SMV, we use rewrite rules and its operational semantics.

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, D.L. Dill, “Symbolic Model Checking for Sequential Circuit Verification,” IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems, Vol.13, No.4, pp.401–424, 1994.

    Article  Google Scholar 

  2. W. Chan, R.J. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, J. D. Reese, “Model checking large software specifications,” IEEE Trans. on Software Engineering, Vol.24, No.7, pp.498–520, 1998.

    Article  Google Scholar 

  3. K. Havelund, T. Pressburger, “Model Checking Java Programs Using Java PathFinder,” To appear in International Journal on Software Tools for Technology Transfer, available at http://ase.arc.nasa.gov/havelund.

  4. J. Staunstrup, et. al., “Practical Verification of Embedded Software,” IEEE Computer, Vol. 33, No. 5, 2000

    Google Scholar 

  5. K.L. McMillan, “Symbolic Model Checking: An approach to the state explosion problem, PhD thesis, Department of Computer Science, Carnegie Mellon University, 1992.

    Google Scholar 

  6. R. Alur and M. Yannakakis, “Model checking of hierarchical state machines,” Proceedings of ACM Symposium on the Foundations of Software Engineering, pp.175–188, 1998

    Google Scholar 

  7. G. Behrmann, et. al., “Verification of hierarchical state/event systems using reusability and compositionality,” Proceedings of TACAS/ETAPS’99, LNCS 1579, pp.163–177, 1999

    Google Scholar 

  8. D. Harel, A. Naamad, “The STATEMATE semantics of statecharts,” ACM Trans. on Software Engineering and Methodology, Vol.5, No.4, pp.293–333, 1996.

    Article  Google Scholar 

  9. N. Day, “A Model Checker for Statecharts,” Master thesis, Department of Computer Science, University of British Columbia, 1993

    Google Scholar 

  10. E. Mikk, Y. Lakhnech, M. Siegel, G.J. Holzmann, “Implementing Statecharts in Pro-mela/SPIN,” Proceedings of the IEEE Workshop on Industrial-Strength Formal Specification Techniques, 1999

    Google Scholar 

  11. W. Damm, B. Josko, H. Hungar, and A. Pnueli, “A compositional real-time semantics of STATEMATE designs,” Proceedings of COMPOS’97, LNCS 1536, pp. 186–238, 1998

    Google Scholar 

  12. W. Heinle, E. Clarke, “STP: translation of statecharts to SMV,” in preparation, 2000

    Google Scholar 

  13. T. Bienmueller, W. Damm, and H. Wittke, The STATEMATE Verification Environment-Making it real,” Proceedings of CAV’00, LNCS 1855, 2000

    Google Scholar 

  14. D. Latella, I. Majzik and M. Massink, “Towards a formal operational semantics of UML statechart diagrams,” The 3rd International Conference on Formal Methods for Open Object-Oriented Distributed Systems, Kluwer Academic Publishers, 1999.

    Google Scholar 

  15. S. Gnesi, D. Latella, M. Massink, “Model checking UML satetchart diagrams using JACK,” Proceedings of the IEEE International Symposium on High Assurance Systems Engineering, 1999.

    Google Scholar 

  16. J. Lilius and I.P. Paltor, “The Semantics of UML State Machines,” Proceedings of ≪UML≫’99 — The Unified Modeling Language, Lecture Notes in Computer Science 1723, 1999.

    Google Scholar 

  17. E. Mikk, Y. Lakhnech, M. Siegel, “Hierarchical automata as model for statecharts,” Pro-ceedings of Asian Computing Science Conference ASIAN’97, Lecture Notes in Computer Science 1345, 1997

    Google Scholar 

  18. C.B. Jones, Systematic Software Development Using VDM, Prentice-Hall, 1986

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Kyonggi University, Suwon-si, Kyonggi-do, Korea

    Gihwon Kwon

Authors
  1. Gihwon Kwon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of York, Y010 5DD, Heslington, York, UK

    Andy Evans

  2. Computing Laboratory, University of Kent, Canterbury, Kent, UK

    Stuart Kent

  3. Rational Software Inc., 340 March Road, Kanata, K2K,2E4, Ontario, Canada

    Bran Selic

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kwon, G. (2000). Rewrite Rules and Operational Semantics for Model Checking UML Statecharts. In: Evans, A., Kent, S., Selic, B. (eds) ≪UML≫ 2000 — The Unified Modeling Language. UML 2000. Lecture Notes in Computer Science, vol 1939. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-40011-7_39

Download citation

  • DOI: https://doi.org/10.1007/3-540-40011-7_39

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41133-8

  • Online ISBN: 978-3-540-40011-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation