|
Vol: 55(69) No: 4 / December 2010 Automated Formal Verification of Graph Rewriting-Based Model Transformations Márk Asztalos Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics, Magyar Tudósok körútja 2. I. em. 1111 Budapest, Hungary, phone: (36) 1-463-24-72, e-mail: asztalos@aut.bme.hu Péter Ekler Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics, Magyar Tudósok körútja 2. I. em. 1111 Budapest, Hungary, e-mail: peter.ekler@aut.bme.hu László Lengyel Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics, Magyar Tudósok körútja 2. I. em. 1111 Budapest, Hungary, e-mail: lengyel@aut.bme.hu Tihamér Levendovszky Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics, Magyar Tudósok körútja 2. I. em. 1111 Budapest, Hungary, e-mail: tihamer@aut.bme.hu István Madari Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics, Magyar Tudósok körútja 2. I. em. 1111 Budapest, Hungary, e-mail: istvan.madari@aut.bme.hu Tamás Vajk Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Faculty of Electrical Engineering and Informatics, Magyar Tudósok körútja 2. I. em. 1111 Budapest, Hungary, e-mail: tamas.vajk@aut.bme.hu Keywords: graph-rewriting, model transformation, verification, metamodeling, rewriting rules Abstract Verification of models and model processing programs has become a fundamental research area in model-based software development. Developers are often interested in offline verification methods, when only the definition of the programs and the specification of the languages that describe the source and target models are used to analyze the properties and no concrete input models are taken into account. Therefore, the results of the analysis hold for each output model not just particular ones, and we have to perform the analysis only once. Graph rewriting-based model transformations are used to specify model processing programs because of their strong mathematical background. Most often, formal verification of model transformations is performed manually or the methods can be applied only for a certain transformation or for the analysis of only a certain property. Previous work has presented formal and algorithmic background for a possible verification framework, which is summarized in this paper. We present a realization of an automated verification framework that is able to automatically perform the offline analysis of graph rewriting-based model transformations and verify certain type of properties that are detailed in the paper. We demonstrate the operation of the framework and its applicability on a case study of refactoring mobile-based social network models. Our results suggest that these methods can be applied in complex real-world solutions as well. References [1] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer, Fundamentals of Algebraic Graph Transformation, vol. XIV of Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2006. [2] M. Asztalos, L. Lengyel, and T. Levendovszky “A Formalism for Describing Modeling Transformations for Verification” in MoDeVVA’09, Denver, Colorado, USA, 2009 [3] M Asztalos, L Lengyel, T Levendovszky “Toward Automated Verification of Model Transformations: A Case Study of Analysis of Refactoring Business Process Models” Workshop on Multi-Paradigm Modeling, Denver, USA, 2009 [4] M. Asztalos, L. Lengyel and T. Levendovszky “Towards Automated Formal Verification of Model Transformations” International Conference on Software Testing, Verification and Validation, Paris, France, 2010 [5] Visual Modeling and Transformation System (VMTS) website: http://vmts.aut.bme.hu [6] L. Angyal, M. Asztalos, L. Lengyel, T. Levendovszky, I. Madari, G. Mezei, T. Mészáros, L. Siroki, and T. Vajk ”Towards a Fast, Efficient and Customizable Domain-Specific Modeling Framework” Software Engineering, Innsbruck, Austria 978-0-88986-785-7, 2009. [7] P. Ekler, T. Lukovszki. “Experiences with Phonebook-Centric Social Networks”. In Proceedings of the 7th IEEE Conference on Consumer Communications and Networking Conference (Las Vegas, Nevada, USA, January 09 - 12, 2010). IEEE Press, Piscataway, NJ, 412-416. [8] M Asztalos, P Ekler, L Lengyel and T Levendovszky “MCDL: A Language for Specifying Graph Conditions with Attribute Constraints” Model-Driven Engineering, Verification, and Validation: Integrating Verification and Validation in MDE, Oslo, Norway, October 3. 2010. (in-press) [9] D. Varró “Towards formal verification of model transformations” PhD Student Workshop of FMOODS 2002, Formal Methods for Open Object-Based Distributed Systems, Enschede, The Netherlands, 2002. [10] G. Karsai and A. Narayanan, “Towards verification of model transformations via goal-directed certification” Model-Driven Development of Reliable Automotive Services: Second Automotive Software Workshop, ASWSD 2006, San Diego, CA, USA, March 15-17, 2006, Revised Selected Papers, pp. 67–83, 2008. [11] D. Bisztray and R. Heckel, “Rule-level verification of business process transformations using CSP,” ECEASST, vol. 6, 2007. [12] J. O. Blech, S. Glesner, and J. Leitner, “Formal Verification of Java Code Generation from UML Models,” in Fujaba Days, Fujaba Days, September 2005. [13] B. Becker, D. Beyer, H. Giese, F. Klein, and D. Schilling, “Symbolic invariant verification for systems with dynamic structural adaptation,” in ICSE \'06: Proceedings of the 28th International Conference on Software Engineering, (New York, NY, USA), pp. 72–81, ACM, 2006. [14] K. Anastasakis, B. Bordbar, and J. M. Küster, “Analysis of Model Transformations via Alloy,” in MoDeVVA\'07, pp. 47–56, October 2007. 17. [15] B. Schatz, “Formalization and Rule-Based Transformation of EMF Ecore-Based Models,” Software Language Engineering: First International Conference, SLE 2008, Toulouse, France, September 29-30, 2008. Revised Selected Papers, pp. 227–244, 2009. [16] K.-H. Pennemann “Development of Correct Graph Transformation Systems” PhD thesis, Department of Computing Science, University of Oldenburg, Oldenburg, 2009. [17] F. Orejas, “Attributed graph constraints,” in ICGT \'08: Proceedings of the 4th international conference on Graph Transformations, (Berlin, Heidelberg), pp. 274–288, Springer-Verlag, 2008. [18] G. Rozenberg, “Handbook on graph grammars and computing by graph transformation, foundations, vol.1,” World Scientific,, 1997. [19] H. Ehrig, K. Ehrig, U. Prange, and G. Taentzer, Fundamentals of Algebraic Graph Transformation, vol. XIV of Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2006. [20] M. Asztalos, “Comparison of termination criteria for graph transformation systems,” in Automation and Applied Computer Science Workshop (AACS), (Budapest, Hungary), 2007. [21] P. Bottoni, K. Hoffmann, F. Parisi Presicce, and G. Taentyer, “High-level replacement units and their termination properties,” Journal of Visual Languages and Computing, vol. 16, pp. 485–507, 2005. [22] H. Ehrig, K. Ehrig, J. de Lara, G. Taentzer, D. Varró, and S. Varró-Gyapay, “Termination criteria for model transformation,” FASE, pp. 49–63, 2005. [23] T. Levendovszky, U. Prange, and H. Ehrig, “Termination criteria for DPO transformations with injective matches,” Electron. Notes Theor. Comput. Sci., vol. 175, no. 4, pp. 87–100, 2007. |