Abstract
We extend a previously proposed symbolic model transformation property prover for the DSLTrans transformation language. The original prover generated the set of path conditions (i.e., symbolic transformation executions), and verified atomic contracts (constraints on input-output model relations) on these path conditions. The prover evaluated atomic contracts to yield either true or false for the transformation when run on any input model. In this paper we extend the prover such that it can verify atomic contracts and more complex properties composed of atomic contracts. Besides demonstrating our prover on a simple transformation, we use it to verify different kinds of properties of an industrial transformation. Experiments on this transformation using our prover show a speed-up in verification run-time by two orders of magnitude over another verification tool that we evaluated in previous research.
This work is supported in part by NSERC, as part of the NECSIS Automotive Partnership with General Motors, IBM Canada and Malina Software Corp.
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
AUTOSAR Consortium. AUTOSAR System Template (2007), http://autosar.org/download/R3.1/AUTOSAR_SystemTemplate.pdf
Amrani, M., Lúcio, L., Selim, G., Combemale, B., Dingel, J., Vangheluwe, H., Le Traon, Y., Cordy, J.R.: A Tridimensional Approach for Studying the Formal Verification of Model Transformations. In: VOLT, pp. 921–928 (2012)
Anastasakis, K., Bordbar, B., Küster, J.: Analysis of Model Transformations via Alloy. MoDeVVa, 47–56 (2007)
Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: Advanced Concepts and Tools for In-Place EMF Model Transformations. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010, Part I. LNCS, vol. 6394, pp. 121–135. Springer, Heidelberg (2010)
Asztalos, M., Lengyel, L., Levendovszky, T.: Formal Specification and Analysis of Functional Properties of Graph Rewriting-Based Model Transformation. Software Testing, Verification and Reliability 23(5), 405–435 (2013)
Baresi, L., Spoletini, P.: On the Use of Alloy to Analyze Graph Transformation Systems. In: Corradini, A., Ehrig, H., Montanari, U., Ribeiro, L., Rozenberg, G. (eds.) ICGT 2006. LNCS, vol. 4178, pp. 306–320. Springer, Heidelberg (2006)
Barroca, B., Lúcio, L., Amaral, V., Félix, R., Sousa, V.: DSLTrans: A Turing Incomplete Transformation Language. In: Malloy, B., Staab, S., van den Brand, M. (eds.) SLE 2010. LNCS, vol. 6563, pp. 296–305. Springer, Heidelberg (2011)
Becker, B., Beyer, D., Giese, H., Klein, F., Schilling, D.: Symbolic Invariant Verification for Systems with Dynamic Structural Adaptation. In: ICSE (2006)
Büttner, F., Egea, M., Guerra, E., De Lara, J.: Checking Model Transformation Refinement. In: ICMT, pp. 158–173 (2013)
Cabot, J., Clarisó, R., Guerra, E., de Lara, J.: Verification and Validation of Declarative Model-to-Model Transformations Through Invariants. Systems and Software 83(2), 283–302 (2010)
Guerra, E., de Lara, J., Kolovos, D., Paige, R.: A Visual Specification Language for Model-to-Model Transformations. In: VL/HCC, pp. 119–126. IEEE (2010)
Lúcio, L., Oakes, B., Vangheluwe, H.: A Technique for Symbolically Verifying Properties of Graph-Based Model Transformations. Technical Report SOCS-TR-2014.1, McGill U (2014)
Lúcio, L., Selim, G.: DSLTrans Property Prover and Example Transformation, http://msdl.cs.mcgill.ca/people/levi/police_station_verification_example.zip
Lúcio, L., Vangheluwe, H.: Model Transformations to Verify Model Transformations. In: VOLT (2013)
Orejas, F., Wirsing, M.: On the Specification and Verification of Model Transformations. In: Palsberg, J. (ed.) Mosses Festschrift. LNCS, vol. 5700, pp. 140–161. Springer, Heidelberg (2009)
Rahim, L.A., Whittle, J.: A Survey of Approaches for Verifying Model Transformations. SoSyM, 1–26 (2013)
Selim, G.M.K., Büttner, F., Cordy, J.R., Dingel, J., Wang, S.: Automated Verification of Model Transformations in the Automotive Industry. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds.) MODELS 2013. LNCS, vol. 8107, pp. 690–706. Springer, Heidelberg (2013)
Selim, G.M.K., Wang, S., Cordy, J.R., Dingel, J.: Model Transformations for Migrating Legacy Models: An Industrial Case Study. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., Störrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 90–101. Springer, Heidelberg (2012)
Syriani, E., Vangheluwe, H.: De-/re-constructing Model Transformation Languages. EASST 29 (2010)
Taentzer, G.: AGG: A Graph Transformation Environment for Modeling and Validation of Software. In: Pfaltz, J.L., Nagl, M., Böhlen, B. (eds.) AGTIVE 2003. LNCS, vol. 3062, pp. 446–453. Springer, Heidelberg (2004)
Troya, J., Vallecillo, A.: A Rewriting Logic Semantics for ATL. JOT 10(5), 1–29 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Selim, G.M.K., Lúcio, L., Cordy, J.R., Dingel, J., Oakes, B.J. (2014). Specification and Verification of Graph-Based Model Transformation Properties. In: Giese, H., König, B. (eds) Graph Transformation. ICGT 2014. Lecture Notes in Computer Science, vol 8571. Springer, Cham. https://doi.org/10.1007/978-3-319-09108-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-09108-2_8
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-09107-5
Online ISBN: 978-3-319-09108-2
eBook Packages: Computer ScienceComputer Science (R0)