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
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
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)
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informaticae 26(3-4), 287–313 (1996)
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. International Journal on Software Tools for Technology Transfer 2(4) (2000)
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)
Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Reading (2003)
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
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)
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)
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)
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)
Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol. 1. World Scientific, Singapore (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)