Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Automated Verification of Model Transformations in the Automotive Industry

  • Conference paper
Model-Driven Engineering Languages and Systems (MODELS 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8107))

Abstract

Many companies have adopted MDD for developing their software systems. Several studies have reported on such industrial experiences by discussing the effects of MDD and the issues that still need to be addressed. However, only a few studies have discussed using automated verification of industrial model transformations. We previously demonstrated how transformations can be used to migrate GM legacy models to AUTOSAR models. In this study, we investigate using automated verification for such industrial transformations. We report on applying an automated verification approach to the GM-to-AUTOSAR transformation that is based on checking the satisfiability of a relational transformation representation, or a transformation model, with respect to well-formedness OCL constraints. An implementation of this approach is available as a prototype for the ATL language. We present the verification results of this transformation and discuss the practicality of using such tools on industrial size problems.

This work was partially funded by the Nouvelles Équipes Program of the Pays de la Loire Region (France), and by NSERC (Canada), 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

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. AUTOSAR Consortium. AUTOSAR System Template, http://AUTOSAR.org/index.php?p=3&up=1&uup=3&uuup=3&uuuup=0&uuuuup=0/AUTOSAR_TPS_SstemTemplate.pdf (2007)

  2. AUTOSAR Consortium. AUTOSAR (2007), http://AUTOSAR.org/

  3. Anastasakis, K., Bordbar, B., Küster, J.: Analysis of Model Transformations via Alloy. MoDeVVa, pp. 47–56 (2007)

    Google Scholar 

  4. Asztalos, M., Lengyel, L., Levendovszky, T.: Towards Automated, Formal Verification of Model Transformations. In: ICST, Paris, France, pp. 15–24 (2010)

    Google Scholar 

  5. 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)

    Chapter  Google Scholar 

  6. Becker, B., Lambers, L., Dyck, J., Birth, S., Giese, H.: Iterative Development of Consistency-Preserving Rule-Based Refactorings. In: Cabot, J., Visser, E. (eds.) ICMT 2011. LNCS, vol. 6707, pp. 123–137. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  7. Braga, C., Menezes, R., Comicio, T., Santos, C., Landim, E.: On the Specification, Verification and Implementation of Model Transformations with Transformation Contracts. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 108–123. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Brucker, A.D., Wolff, B.: Semantics, Calculi, and Analysis for Object-Oriented Specifications. Acta Informatica 46(4), 255–284 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  9. Büttner, F., Egea, M., Cabot, J.: On verifying ATL Transformations Using ‘Off-the-Shelf’ SMT Solvers. In: France, R.B., Kazmeier, J., Breu, R., Atkinson, C. (eds.) MODELS 2012. LNCS, vol. 7590, pp. 432–448. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  10. Büttner, F., Egea, M., Cabot, J., Gogolla, M.: Verification of ATL Transformations Using Transformation Models and Model Finders. In: Aoki, T., Taguchi, K. (eds.) ICFEM 2012. LNCS, vol. 7635, pp. 198–213. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  11. 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)

    Article  Google Scholar 

  12. Cariou, E., Belloir, N., Barbier, F., Djemam, N.: OCL Contracts for the Verification of Model Transformations. EASST 24 (2009)

    Google Scholar 

  13. Cottenier, T., Van Den Berg, A., Elrad, T.: The Motorola WEAVR: Model Weaving in a Large Industrial Context. In: AOSD, Vancouver, Canada, vol. 32 (2007)

    Google Scholar 

  14. Daghsen, A., Chaaban, K., Saudrais, S., Leserf, P.: Applying Holistic Distributed Scheduling to AUTOSAR Methodology. In: ERTSS, Toulouse, France (2010)

    Google Scholar 

  15. Giese, H., Hildebrandt, S., Neumann, S.: Model Synchronization at Work: Keeping sysML and AUTOSAR Models Consistent. In: Engels, G., Lewerentz, C., Schäfer, W., Schürr, A., Westfechtel, B. (eds.) Nagl Festschrift. LNCS, vol. 5765, pp. 555–579. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  16. Gogolla, M., Vallecillo, A.: Tractable Model Transformation Testing. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 221–235. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  17. González Pérez, C.A., Büttner, F., Clarisó, R., Cabot, J.: EMFtoCSP: A Tool for the Lightweight Verification of EMF Models. In: FormSERA, Zurich, Switzerland, pp. 44–50 (2012)

    Google Scholar 

  18. Guerra, E., de Lara, J., Wimmer, M., Kappel, G., Kusel, A., Retschitzegger, W., Schönböck, J., Schwinger, W.: Automated Verification of Model Transformations Based on Visual Contracts. Automated Software Engineering 20(1), 5–46 (2013)

    Article  Google Scholar 

  19. Inaba, K., Hidaka, S., Hu, Z., Kato, H., Nakano, K.: Graph-Transformation Verification Using Monadic Second-Order Logic. In: PPDP, pp. 17–28 (2011)

    Google Scholar 

  20. Jackson, E., Levendovszky, T., Balasubramanian, D.: Automatically reasoning about metamodeling. SoSyM, pp. 1–15 (2013)

    Google Scholar 

  21. Jacobs, B., Poll, E.: A Logic for the Java Modeling Language JML. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 284–299. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  22. Jouault, F., Allilaire, F., Bézivin, J., Kurtev, I.: ATL: A Model Transformation Tool. Sci. Comput. Program. 72(1-2), 31–39 (2008)

    Article  MATH  Google Scholar 

  23. Kuhlmann, M., Hamann, L., Gogolla, M.: Extensive Validation of OCL Models by Integrating SAT Solving into USE. In: Bishop, J., Vallecillo, A. (eds.) TOOLS 2011. LNCS, vol. 6705, pp. 290–306. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  24. Lúcio, L., Barroca, B., Amaral, V.: A Technique for Automatic Validation of Model Transformations. In: Petriu, D.C., Rouquette, N., Haugen, Ø. (eds.) MODELS 2010, Part I. LNCS, vol. 6394, pp. 136–150. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  25. Mohagheghi, P., Dehlen, V.: Where is the Proof? - A Review of Experiences from Applying MDE in Industry. In: Schieferdecker, I., Hartman, A. (eds.) ECMDA-FA 2008. LNCS, vol. 5095, pp. 432–443. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. Narayanan, A., Karsai, G.: Verifying Model Transformations by Structural Correspondence. EASST 10 (2008)

    Google Scholar 

  27. Queralt, A., Teniente, E.: Verification and Validation of UML Conceptual Schemas with OCL Constraints. TOSEM 21(2), 13 (2012)

    Google Scholar 

  28. Rensink, A.: Explicit State Model Checking for Graph Grammars. In: Degano, P., De Nicola, R., Meseguer, J. (eds.) Concurrency, Graphs and Models. LNCS, vol. 5065, pp. 114–132. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  29. 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)

    Chapter  Google Scholar 

  30. Sen, S., Moha, N., Baudry, B., Jézéquel, J.-M.: Meta-model Pruning. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 32–46. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  31. Stenzel, K., Moebius, N., Reif, W.: Formal Verification of QVT Transformations for Code Generation. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 533–547. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  32. Tisi, M., Jouault, F., Fraternali, P., Ceri, S., Bézivin, J.: On the Use of Higher-Order Model Transformations. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 18–33. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  33. Torlak, E., Jackson, D.: Kodkod: A Relational Model Finder. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 632–647. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  34. Troya, J., Vallecillo, A.: A Rewriting Logic Semantics for ATL. Journal of Object Technology 10(5), 1–29 (2011)

    Google Scholar 

  35. The USE Validator, http://sourceforge.net/projects/useocl/files/Plugins/ModelValidator/

  36. The ATL Transformation Zoo, http://www.eclipse.org/atl/atlTransformations/ .

Download references

Author information

Authors and Affiliations

  1. School of Computing, Queen’s University, Kingston, Ontario, Canada

    Gehan M. K. Selim, James R. Cordy & Juergen Dingel

  2. AtlanMod, École des Mines de Nantes - INRIA, LINA, Nantes, France

    Fabian Büttner

  3. Electrical and Controls Integration Lab., General Motors Research and Development, Warren, Michigan, USA

    Shige Wang

Authors
  1. Gehan M. K. Selim
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fabian Büttner
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. James R. Cordy
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Juergen Dingel
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Shige Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculdade de Ciências e Tecnologia, Departamento de Informática, Universidade Nova de Lisboa, 2829-516, Caparica, Portugal

    Ana Moreira

  2. Institut für Mathematik, fortiss / Technische Universität München, Guerickestraße 25, 80805, München, Germany

    Bernhard Schätz

  3. Department of Computer Science, University of Alabama, Box 870290, 35487-0290, Tuscaloosa, AL, USA

    Jeff Gray

  4. ETSI Informática, Universidad de Málaga, Campus de Teatinos, Bulevar Louis Pasteur 35, 29071, Málaga, Spain

    Antonio Vallecillo

  5. School of Computing and Information Sciences, College of Engineering and Computing, Florida International University, 33199, Miami, FL, USA

    Peter Clarke

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Selim, G.M.K., Büttner, F., Cordy, J.R., Dingel, J., Wang, S. (2013). Automated Verification of Model Transformations in the Automotive Industry. In: Moreira, A., Schätz, B., Gray, J., Vallecillo, A., Clarke, P. (eds) Model-Driven Engineering Languages and Systems. MODELS 2013. Lecture Notes in Computer Science, vol 8107. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-41533-3_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-41533-3_42

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-41532-6

  • Online ISBN: 978-3-642-41533-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation