Abstract
Model transformations are first-class artifacts in a model-driven development process. As such, their verification and validation is an important task. We have been developing a technique to specify, verify, validate and implement model transformations. Our technique is based on the concept of transformation contracts, a specification that relates two modeling languages and declares properties that must be fulfilled in such a relation. A transformation contract is essentially a transformation model that allows for the verification and validation of a model transformation using the same techniques one uses to verify and validate any given model. This paper describes our technique, discusses consistency of model transformations and reports on its application to a model transformation from access control models to Java security.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Akehurst, D.H., Kent, S.: A relational approach to defining transformations in a metamodel. In: Jézéquel, J.-M., Hussmann, H., Cook, S. (eds.) UML 2002. LNCS, vol. 2460, pp. 243–258. Springer, Heidelberg (2002)
Baader, F., Diego Calvanese, D.M., Nardi, D., Patel-Schneider, P.: The Description Logic Handbook. Cambridge University Press (2003)
Basin, D., Clavel, M., Doser, J., Egea, M.: Automated analysis of security-design models. Inf. Softw. Technol. 51(5), 815–831 (2009)
Basin, D., Doser, J., Lodderstedt, T.: Model driven security: From uml models to access control infrastructures. ACM Trans. Softw. Eng. Methodol. 15(1), 39–91 (2006)
Berardi, D., Calvanese, D., Giacomo, G.D.: Reasoning on UML class diagrams. Artif. Intellig. 168, 70–118 (2005)
Bézivin, J., Büttner, F., Gogolla, M., Jouault, F., Kurtev, I., Lindow, A.: Model Transformations? Transformation Models! In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MoDELS 2006. LNCS, vol. 4199, pp. 440–453. Springer, Heidelberg (2006)
Braga, C.: From access control policies to an aspect-based infrastructure: A metamodel-based approach. In: Chaudron, M.R.V. (ed.) MODELS 2008. LNCS, vol. 5421, pp. 243–256. Springer, Heidelberg (2009)
Braga, C.: A transformation contract to generate aspects from access control policies. J. of Software and Systems Modeling (2010), doi:10.1007/s10270-010-0156-x
Braga, C., Hæusler, E.H.: Lightweight analysis of access control models with description logic. Innov. in Systems and Soft. Eng. 6, 115–123 (2010)
Cariou, E., Marvie, R., Seinturier, L., Duchien, L.: OCL for the specification of model transformation contracts. In: Proc. of OCL and Model Driven Eng. Work., pp. 69–83 (2004)
Clavel, M., Egea, M., de Dios Miguel Angel, G.: Building an efficient component for OCL evaluation. ECEASST 15 (2008)
Comicio, T.: A transformation contract approach for model-driven security. Master’s thesis, Universidade Federal Fluminense (2011)
Egea, M.: An Executable Formal Semantics for OCL with Applications to Model Analysis and Validation. PhD thesis, Universidad Complutense de Madrid (2008)
Gorp, P.V., Janssens, D.: Cavit: a consistency maintenance framework based on transformation contracts. In: Transformation Techniques in Soft. Eng., Dagstuhl Seminar Proc., vol. 05161 (2006)
Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained. Addison-Wesley, Reading (2003)
OMG. MOF QVT final adopted specification, omg adopted specification ptc/05-11-01 (2005)
Schürr, A.: Specification of graph translators with triple graph grammars. In: Mayr, E.W., Schmidt, G., Tinhofer, G. (eds.) WG 1994. LNCS, vol. 903, pp. 151–163. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Braga, C., Menezes, R., Comicio, T., Santos, C., Landim, E. (2011). On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts. In: Simao, A., Morgan, C. (eds) Formal Methods, Foundations and Applications. SBMF 2011. Lecture Notes in Computer Science, vol 7021. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-25032-3_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-25032-3_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-25031-6
Online ISBN: 978-3-642-25032-3
eBook Packages: Computer ScienceComputer Science (R0)