Test-driven verification/validation of model transformations

Abstract

Why is it important to verify/validate model transformations? The motivation is to improve the quality of the transformations, and therefore the quality of the generated software artifacts. Verified/validated model transformations make it possible to ensure certain properties of the generated software artifacts. In this way, verification/validation methods can guarantee different requirements stated by the actual domain against the generated/modified/optimized software products. For example, a verified/validated model transformation can ensure the preservation of certain properties during the model-to-model transformation. This paper emphasizes the necessity of methods that make model transformation verified/validated, discusses the different scenarios of model transformation verification and validation, and introduces the principles of a novel test-driven method for verifying/validating model transformations. We provide a solution that makes it possible to automatically generate test input models for model transformations. Furthermore, we collect and discuss the actual open issues in the field of verification/validation of model transformations.

Keywords

Graph rewriting based model transformations / Verification/validation / Test-driven verification

References

[1] Akehurst, D., Kent, S., 2002. A relational approach to defining transformations in a metamodel. LNCS, 2460: 243-258. [

[2] Amrani, M., Dingel, J., Lambers, L., , 2012. Towards a model transformation intent catalog. Proc. 1st Workshop on the Analysis of Model Transformations, p.3-8. [

[3] Assmann, U., 1996. How to uniformly specify program analysis and transformation with graph rewrite systems. LNCS, 1060: 121-135. [

[4] Assmann, U., Ludwig, A., 2000. Aspect weaving with graph rewriting. LNCS, 1799: 24-36. [

[5] Asztalos, M., Lengyel, L., Levendovszky, T., 2010a. Towards automated, formal verification of model transformations. IEEE Int. Conf. on Software Testing V&V, p.15-24.

[6] Asztalos, M., Ekler, P., Lengyel, L., , 2010b. Applying online verification of model transformations to mobile social networks. Electronic Communications of the EASST. Proc. 4th Int. Workshop on Graph-Based Tools.

[7] Blostein, D., Fahmy, H., Grbavec, A., 1996. Issues in the practical use of graph rewriting. LNCS, 1073: 38-55. [

[8] Czarnecki, K., Helsen, S., 2006. Feature-based survey of model transformation approaches. IBM Syst. J., 45(3): 621-646. [

[9] de Lara, J., Taentzer, G., 2004. Automated model transformation and its validation using AToM₃ and AGG. LNCS, 2980: 182-198. [

[10] de Lara, J., Vangheluwe, H., Alfonseca, M., 2004. Metamodelling and graph grammars for multiparadigm modelling in AToM. Softw. Syst. Model., 3(3): 194-209. [

[11] Ehrig, H., Habel, A., Kreowski, H.J., , 1991a. From graph grammars to high level replacement systems. LNCS, 532: 269-291. [

[12] Ehrig, H., Habel, A., Kreowski, H.J., , 1991b. Parallelism and concurrency in high-level replacement systems. Math. Struct. Comput. Sci., 1(3): 361-404.

[13] Ehrig, H., Engels, G., Kreowski, H.J., (Eds.), 1999. Handbook on Graph Grammars and Computing by Graph Transformation: Application, Languages and Tools. World Scientific, Singapore.

[14] Ehrig, H., Habel, A., Padberg, J., , 2004. Adhesive high-level replacement categories and systems. LNCS, 3256: 144-160. [

[15] Ehrig, H., Ehrig, K., Prange, U., , 2006. Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science, Springer.

[16] Giese, H., Glesner, S., Leitner, J., , 2006. Towards verified model transformations. ModeVVa Workshop Associated to MODELS, p.78-93.

[17] Guerra, E., de Lara, J., 2007. Event-driven grammars: relating abstract and concrete levels of visual languages. Softw. Syst. Model., 6(3): 317-347. [

[18] Habel, A., Heckel, R., Taentzer, G., 1996. Graph grammars with negative application conditions. Fundam. Inform., 26: 287-313.

[19] Hetzel, W.C., 1998. The Complete Guide to Software Testing (2nd Ed.). Wiley.

[20] Kaner, C., 2006. Exploratory testing. Quality Assurance Institute Worldwide Annual Software Testing Conf.

[21] Kaner, C., Falk, J., Nguyen, H.Q., 1990. Testing Computer Software (2nd Ed.). Wiley, New York.

[22] Karsai, G., Agrawal, A., Shi, F., , 2003. On the use of graph transformation in the formal specification of model interpreters. J. Univ. Comput. Sci., 9(11): 1296-1321.

[23] Kolawa, A., Huizinga, D., 2007. Automated Defect Prevention: Best Practices in Software Management. Wiley-IEEE Computer Society Press, p.41-43.

[24] Lack, S., Sobocinski, P., 2004. Adhesive categories. LNCS, 2987: 273-288.

[25] Leitner, A., Ciupa, I., Oriol, M., , 2007. Contract Driven Development= Test Driven Development - Writing Test Cases. Proc. 6th Joint Meeting of the European Software Engineering Conf. and the ACM SIGSOFT Symp. on the Foundations of Software Engineering, p.425-434. [

[26] Lengyel, L., 2006. Online Validation of Visual Model Transformations. PhD Thesis, Department of Automation and Applied Informatics, Budapest University of Technology and Economics, Budapest, Hungary.

[27] Mens, T., van Gorp, P., 2006. A taxonomy of model transformation. Proc. Int. Workshop on Graph and Model Transformation, p.125-142.

[28] Narayanan, A., Karsai, G., 2008. Towards verifying model transformations. Electron. Notes Theor. Comput. Sci., 211: 191-200. [

[29] OMG, 2010. Unified Modeling Language (UML) Specification, Version 2.3, OMG document formal/2010-05-03, Available from http://www.uml.org/.

[30] OMG, 2011. OMG Query/View/Transformation (QVT) Specification, Meta Object Facility 2.0 Query/Views/Transformation Specification. OMG doc. formal/2011.01.01. Available from http://www.omg.org/spec/QVT/.

[31] OMG, 2012. OMG Object Constraint Language (OCL) Specification, Version 2.3.1. OMG Document Formal/2012-05-09. Available from http://www.omg.org/spec/OCL/.

[32] OMG, 2014. OMG Model-Driven Architecture (MDA) Specification. OMG Document ormsc/14-06-01. Available from http://www.omg.org/mda/.

[33] Pan, J., 1999. Software Testing- 18-849b Dependable Embedded Systems. Carnegie Mellon University. Available from http://users.ece.cmu.edu/~koopman/des_s99/sw_testing/.

[34] Plump, D., 1998. Termination of graph rewriting is undecidable. Fundam. Inf., 33(2): 201-209.

[35] Rozenberg, G. (Ed.), 1997. Handbook on Graph Grammars and Computing by Graph Transformation: Foundations. World Scientific, Singapore.

[36] Schürr, A., 1994. Specification of graph translators with triple graph grammars. LNCS, 903: 151-163. [

[37] Syriani, E., 2009. Matters of Model Transformation. No. SOCS-TR-2009.2, School of Computer Science, McGill University.

[38] Taentzer, G., Ehrig, K., Guerra, E., , 2005. Model transformation by graph transformation: a comparative study. ACM/IEEE 8th Int. Conf. on Model Driven Engineering Languages and Systems, p.1-48.

[39] Vajk, T., Kereskényi, R., Levendovszky, T., , 2009. Raising the abstraction of domain-specific model translator development. 16th Annual IEEE Int. Conf. and Workshop on the Engineering of Computer Based Systems, p.31-37. [

[40] van Gorp, P., Stenten, H., Mens, T., , 2003. Towards automating source-consistent UML refactorings. LNCS, 2863: 144-158. [

[41] Varró, D., Pataricza, A., 2003. Automated formal verification of model transformations. Proc. UML03 Workshop, p.63-78.

[42] Varró, D., Varró-Gyapay, S., Ehrig, H., , 2006. Termination analysis of model transformations by Petri nets. LNCS, 4178: 260-274. [