Skip to main content
SpringerLink
Log in

Model Checking Dynamic States in GROOVE

  • Conference paper
Model Checking Software (SPIN 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3925))

Included in the following conference series:

Abstract

Much research has been done in the field of model-checking complex systems (either hardware or software). Approaches that use explicit state modelling mostly use bit vectors to represent the states of such systems. Unfortunately, that kind of representation does not extend smoothly to systems in which the states contain values from a domain other than primitive types, such as reference values commonly used in object-oriented systems.

In this paper we report preliminary results on applying CTL model checking on state spaces generated using graph transformations. The states of such state spaces have an internal graph structure which makes it possible to represent complex system states without the need to know the exact structure beforehand as when using bit vectors.

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. Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: 29th Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages (POPL), pp. 1–3. ACM Press, New York (2002)

    Google Scholar 

  2. Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Trans. Softw. Eng. 30(6), 388–402 (2004)

    Article  Google Scholar 

  3. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)

    Chapter  Google Scholar 

  4. Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informaticae 26(3-4), 287–313 (1996)

    MathSciNet  MATH  Google Scholar 

  5. Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4) (2000)

    Google Scholar 

  6. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 235–239. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  7. Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2003)

    Google Scholar 

  8. Kastenberg, H., Kleppe, A., Rensink, A.: Engineering object-oriented semantics using graph transformations. Technical report, Department of Computer Science, University of Twente (2005), Pre-final version available at, http://www.cs.utwente.nl/~rensink/papers/taal-draft.pdf

  9. Rensink, A.: The GROOVE simulator: A tool for state space generation. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 479–485. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  10. Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 319–335. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Rensink, A.: Time and space issues in the generation of graph transition systems. In: International Workshop on Graph-Based Tools (GraBaTs). Electronic Notes in Theoretical Computer Science, vol. 127, pp. 127–139 (2005)

    Google Scholar 

  12. Rensink, A., Distefano, D.: Abstract graph transformation. In: International Workshop on Software Verification and Validation (SVV). Electronic Notes in Theoretical Computer Science (2005); Technical report version: CTITTR–CTIT–05–04, University of Twente (to appear)

    Google Scholar 

  13. Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol. 1. World Scientific, Singapore (1997)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Twente, P.O. Box 217, 7500 AE, Enschede, The Netherlands

    Harmen Kastenberg & Arend Rensink

Authors
  1. Harmen Kastenberg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Arend Rensink
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Software Systems, Tampere University of Technology, PO Box 553, FI-33101, Tampere, Finland

    Antti Valmari

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kastenberg, H., Rensink, A. (2006). Model Checking Dynamic States in GROOVE. In: Valmari, A. (eds) Model Checking Software. SPIN 2006. Lecture Notes in Computer Science, vol 3925. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691617_19

Download citation

  • DOI: https://doi.org/10.1007/11691617_19

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-33102-5

  • Online ISBN: 978-3-540-33103-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation