Skip to main content
SpringerLink
Log in
SpringerLink
Log in

A Formal Framework for Prototyping Executable Semantics in ATL

  • Conference paper
  • First Online:
Theory and Practice of Model Transformation (ICMT 2018)

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

  • 510 Accesses

Abstract

ATL is a well-established model transformation language both in industry and in academia, where it is used as a reference language for studying different types of model transformations and their properties. In this paper, we discuss current limitations of ATL’s in-place semantics that hamper its application for modelling and verifying systems and propose a new in-place semantics for ATL that enables it as a specification language for simulating and verifying EMF-based systems. Our approach is based on FMA-ATL, an executable specification of a large excerpt of ATL in Maude, which has been augmented with the new in-place semantics so that Maude’s verification tools can then be used both to perform bounded model checking of invariants and to model check LTL formulas in the resulting system models, where appropriate. Furthermore, FMA-ATL uses ATL as front-end language and it can be reused as-is for verification, including its tool support.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
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 EPUB and 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

Notes

  1. 1.

    Internally FMA-ATL works with a term representation of engine configurations and system states, which is depicted graphically for the sake of presentation.

  2. 2.

    Using =>* the search will be performed along zero or many simulation steps. However, other strategies that can be used are =>! for run to completion semantics, =>1 for one step, =>+ for at least one step.

  3. 3.

    https://fma-atl.github.io.

  4. 4.

    http://wiki.eclipse.org/Henshin/State_Space_Tools.

References

  1. 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. LNCS, vol. 6394, pp. 121–135. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16145-2_9

    Chapter  Google Scholar 

  2. Boronat, A.: Experimentation with a big-step semantics for ATL model transformations. In: Guerra, E., van den Brand, M. (eds.) ICMT 2017. LNCS, vol. 10374, pp. 3–18. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-61473-1_1

    Chapter  Google Scholar 

  3. Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1

    Book  MATH  Google Scholar 

  4. Cuadrado, J.S., Guerra, E., de Lara, J.: Uncovering errors in ATL model transformations using static analysis and constraint solving. In: ISSRE, pp. 34–44. IEEE Computer Society (2014)

    Google Scholar 

  5. Durán, F., Moreno-Delgado, A., Álvarez-Palomo, J.M.: Statistical model checking of e-motions domain-specific modeling languages. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 305–322. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49665-7_18

    Chapter  Google Scholar 

  6. Eker, S., Meseguer, J., Sridharanarayanan, A.: The maude LTL model checker. Electr. Notes Theor. Comput. Sci. 71, 162–187 (2002)

    Article  Google Scholar 

  7. Ghamarian, A.H., de Mol, M., Rensink, A., Zambon, E., Zimakova, M.: Modelling and analysis using GROOVE. STTT 14(1), 15–40 (2012)

    Article  Google Scholar 

  8. Roldán, M., Durán, F.: The mOdCL evaluator: Maude + OCL (2013). http://maude.lcc.uma.es/mOdCL/. Accessed 3 Mar 2016

  9. Rensink, A., Schmidt, Á., Varró, D.: Model checking graph transformations: a comparison of two approaches. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 226–241. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30203-2_17

    Chapter  MATH  Google Scholar 

  10. Tisi, M., Martínez, S., Jouault, F., Cabot, J.: Refining Models with Rule-based Model Transformations. Research Report RR-7582, March 2011

    Google Scholar 

  11. Troya, J., Rivera, J.E., Vallecillo, A.: Simulating domain specific visual models by observation. In: SpringSim, p. 128. SCS/ACM (2010)

    Google Scholar 

  12. Wagelaar, D., Tisi, M., Cabot, J., Jouault, F.: Towards a general composition semantics for rule-based model transformation. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 623–637. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24485-8_46

    Chapter  Google Scholar 

Download references

Acknowledgements

The author would like to thank Frédéric Jouault and Massimo Tisi for insightful discussions on the semantics of ATL, and the anonymous reviewers for their observations, which helped improve this work greatly.

Author information

Authors and Affiliations

  1. Department of Informatics, University of Leicester, Leicester, UK

    Artur Boronat

Authors
  1. Artur Boronat
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Artur Boronat .

Editor information

Editors and Affiliations

  1. University of Twente, Enschede, The Netherlands

    Arend Rensink

  2. University of Murcia, Murcia, Spain

    Jesús Sánchez Cuadrado

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Boronat, A. (2018). A Formal Framework for Prototyping Executable Semantics in ATL. In: Rensink, A., Sánchez Cuadrado, J. (eds) Theory and Practice of Model Transformation. ICMT 2018. Lecture Notes in Computer Science(), vol 10888. Springer, Cham. https://doi.org/10.1007/978-3-319-93317-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-93317-7_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-93316-0

  • Online ISBN: 978-3-319-93317-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation