Similar articles

Abstract: graph transformation systems have become a general formal modeling language to describe many models in software development process. Behavioral modeling of dynamic systems and model-to-model transformations are only a few examples in which graphs have been used to software development. But even the perfect graph transformation system must be equipped with automated analysis capabilities to let users understand whether such a formal specification fulfills their requirements. In this paper, we present a new solution to verify graph transformation systems using the bogor model checker. The attributed graph grammars (AGG)-like graph transformation systems are translated to Bandera intermediate representation (BIR), the input language of bogor, and bogor verifies the model against some interesting properties defined by combining linear temporal logic (LTL) and special-purpose graph rules. Experimental results are encouraging, showing that in most cases our solution improves existing approaches in terms of both performance and expressiveness.

[1] Baldan, P., König, B., 2002. Approximating the behavior of graph transformation systems. LNCS, 2505:14-29.

[2] Baldan, P., Corradini, A., König, B., 2004a. Verifying finite-state graph grammars: an unfolding-based approach. LNCS, 3170:83-98.

[3] Baldan, P., Corradini, A., Gadducci, F., 2004b. Specifying and verifying UML activity diagrams via graph transformation. LNCS, 3267:18-33.

[4] Baresi, L., Heckel, R., 2002. Tutorial introduction to graph transformation: a software engineering perspective. LNCS, 2505:402-429.

[5] Baresi, L., Spoletini, P., 2006. On the use of Alloy to analyze graph transformation systems. LNCS, 4178:306-320.

[6] Baresi, L., Heckel, R., Thöne, S., Varró, D., 2003. Modeling and Validation of Service Oriented Architectures: Application vs. Style. European Software Engineering Conf. and ACM SIGSOFT Symp. on the Foundations of Software Engineering, p.68-77.

[7] Baresi, L., Heckel, R., Thöne, S., Varró, D., 2006. Style-based modeling and refinement of service-oriented architectures: a graph transformation-based approach. Software Syst. Model., 5(2):187-207.

[8] Baresi, L., Rafe, V., Rahmani, A.T., Spoletini, P., 2008. An Efficient Solution for Model Checking Graph Transformation Systems. 3rd Workshop on Graph Transformation for Verification and Concurrency, ENTCS, 213:3-21.

[9] Bensalem, S., Ganesh, V., Lakhnech, Y., Munoz, C., Owre, S., Rueß, H., Rushby, J., Rusu, V., Saϊdi, H., Shankar, N., et al., 2000. An Overview of SAL. Fifth NASA Langley Formal Methods Workshop, p.187-196.

[10] Compton, K., Gurevich, Y., Huggins, J., Shen, W., 2000. An Automatic Verification Tool for UML. Technical Report, CSE-TR-423-00, Department of Electrical Engineering and Computer Sciences, University of Michigan, USA.

[11] Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H., 2000. Bandera: Extracting Finite-state Models from Java Source Code. 22nd Int. Conf. on Software Engineering, p.439-448.

[12] Dotti, F.L., Foss, L., Ribeiro, L., Santos, O.M., 2003. Verification of object-based distributed systems. LNCS, 2884:261-275.

[13] Ehrig, H., Pfender, M., Schneider, H.J., 1973. Graph Grammars: An Algebraic Approach. 14th Annual Symp. on Switching and Automata Theory, p.167-180.

[14] Ehrig, H., Engels, G., Kreowski, H., Rozenberg, G. (Eds.), 1999. Handbook on Graph Grammars and Computing by Graph Transformation: Applications, Languages and Tools. World Scientific, USA.

[15] Engels, G., Soltenborn, C., Wehrheim, H., 2007. Analysis of UML activities using dynamic meta modeling. LNCS, 4468:76-90.

[16] Ferreira, A.P.L., Foss, L., Ribeiro, L., 2007. Formal Verification of Object-oriented Graph Grammars Specifications. Proc. Third Workshop on Structural Operational Semantics, ENTCS, 175:101-114.

[17] Grunske, L., Winter, K., Yatapanage, N., 2008. Defining the abstract syntax of visual languages with advanced graph grammars—a case study based on behavior trees. J. Vis. Lang. Comput., 19(3):343-379.

[18] Gyapay, S., Schmidt, Á., Varró, D., 2004. Joint Optimization and Reachability Analysis in Graph Transformation Systems with Time. Int. Workshop on Graph Transformation and Visual Modeling Techniques, 109:137-147.

[19] Hausmann, J.H., 2005. Dynamic Meta Modeling: A Semantics Description Technique for Visual Modeling Languages. PhD Thesis, University of Paderborn, Germany.

[20] Hausmann, J.H., Heckel, R., Taentzer, G., 2002. Detection of Conflicting Functional Requirements in a Use Case-driven Approach: A Static Analysis Technique Based on Graph Transformation. Proc. 24th Int. Conf. on Software Engineering, p.105-115.

[21] Heckel, R., 1998. Compositional verification of reactive systems specified by graph transformation. LNCS, 1382:138-153.

[22] Holzmann, G.J., 1997. The model checker SPIN. IEEE Trans. Software Eng., 23(5):279-295.

[23] Jackson, D., 2006. Software Abstractions: Logic, Language, and Analysis. The MIT Press, USA.

[24] Kastenberg, H., 2005. Towards Attributed Graphs in GROOVE. First Workshop on Graph Transformation for Verification and Concurrency, ENTCS, 154:47-54.

[25] Kuske, S., 2001. A formal semantics of UML state machines based on structured graph transformation. LNCS, 2185:241-256.

[26] Latella, D., Majzik, I., Massink, M., 1999. Automatic verification of UML statechart diagrams using the SPIN model checker. Formal Aspects Comput., 11(6):637-664.

[27] Liu, H., Ma, Z.Y., Shao, W.Z., 2007. Description and proof of property preservation of model transformations. J. Software, 18(10):2369-2379.

[28] Paltor, I., Lilius, J., 1999. vUML: A Tool for Verifying UML Models. 14th IEEE Int. Conf. on Automated Software Engineering, p.255-258.

[29] Rafe, V., Rahmani, A.T., 2008. Formal analysis of workflows using UML 2.0 activities and graph transformation systems. LNCS, 5160:305-318.

[30] Rensink, A., 2004. The GROOVE simulator: a tool for state space generation. LNCS, 3062:479-485.

[31] Rensink, A., Schmidt, Á., Varró, D., 2004. Model checking graph transformations: a comparison of two approaches. LNCS, 3256:226-241.

[32] Robby, Dwyer, M.B., Hatcliff, J., 2003. Bogor: an extensible and highly-modular software model checking framework. ACM SIGSOFT Software Eng. Notes, 28(5):267-276.

[33] Schmidt, Á., 2004. Model Checking of Visual Modeling Languages. MS Thesis, Budapest University of Technology, Hungary.

[34] Schmidt, Á., Varró, D., 2003. CheckVML: a tool for model checking visual modeling languages. LNCS, 2863:92-95.