Abstract
Graph transformation systems are a general specification language for systems with dynamically changing topologies, such as mobile and distributed systems. We propose a counterexample-guided abstraction refinement technique which is based on the over-approximation of graph transformation systems (gts) by Petri nets. We show that a spurious counterexample is caused by merging nodes during the approximation. We present a technique for identifying these merged nodes and splitting them using abstraction refinement, which removes the spurious run. The technique has been implemented in the Augur tool and experimental results are discussed.
Research supported by DFG project SANDS and SFB 627 (NEXUS).
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Jonsson, B., Kindahl, M., Peled, D.: A general approach to partial order reductions in symbolic verification. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 379–390. Springer, Heidelberg (1998)
Baldan, P., Corradini, A., Esparza, J., Heindel, T., König, B., Kozioura, V.: Verifying red-black trees. In: Proc. of COSMICAH 2005, Proceedings available as report RR-05-04 (Queen Mary, University of London) (2005)
Baldan, P., Corradini, A., König, B.: A static analysis technique for graph transformation systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 381–395. Springer, Heidelberg (2001)
Baldan, P., Corradini, A., König, B.: Static analysis of distributed systems with mobility specified by graph grammars - a case study. In: Proc. of IDPT 2002. Society for Design and Process Science (2002)
Baldan, P., König, B.: Approximating the behaviour of graph transformation systems. In: Corradini, A., Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) ICGT 2002. LNCS, vol. 2505, pp. 14–29. Springer, Heidelberg (2002)
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: Proc. of ICSE 2003, pp. 385–395. IEEE Computer Society, Los Alamitos (2003)
Clarke, E., Grumberg, S., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Dotti, F.L., Foss, L., Ribeiro, L., Marchi Santos, O.: Verification of distributed object-based systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol. 2884, pp. 261–275. Springer, Heidelberg (2003)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of POPL 2002, pp. 58–70. ACM Press, New York (2002)
König, B., Kozioura, V.: Counterexample-guided abstraction refinement for the analysis of graph transformation systems. Technical Report 01/2006, Universität at Stuttgart (2006)
Loginov, A., Reps, T., Sagiv, M.: Abstraction refinement via inductive learning. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 519–533. Springer, Heidelberg (2005)
Rensink, A.: Canonical graph shapes. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 401–415. Springer, Heidelberg (2004)
Rensink, A.: State space abstraction using shape graphs. In: Proc. of AVIS 2004 (2004) (to appear)
Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformation. Foundations, vol. 1. World Scientific, Singapore (1997)
Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. TOPLAS 24(3), 217–298 (2002)
Varró, D.: Towards symbolic analysis of visual modeling languages. In: Proc. Of GT-VMT 2002. ENTCS, vol. 72. Elsevier, Amsterdam (2002)
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
König, B., Kozioura, V. (2006). Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation Systems. In: Hermanns, H., Palsberg, J. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2006. Lecture Notes in Computer Science, vol 3920. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11691372_13
Download citation
DOI: https://doi.org/10.1007/11691372_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33056-1
Online ISBN: 978-3-540-33057-8
eBook Packages: Computer ScienceComputer Science (R0)