Skip to main content
SpringerLink
Log in
Book cover

International Conference on Model Driven Engineering Languages and Systems

MODELS 2013: Model-Driven Engineering Languages and Systems pp 336–351Cite as

Formal Verification Integration Approach for DSML

  • Conference paper

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

Abstract

The application of formal methods (especially, model checking and static analysis techniques) for the verification of safety critical embedded systems has produced very good results and raised the interest of system designers up to the application of these technologies in real size projects. However, these methods usually rely on specific verification oriented formal languages that most designers do not master. It is thus mandatory to embed the associated tools in automated verification toolchains that allow designers to rely on their usual domain-specific modeling languages (DSMLs) while enjoying the benefits of these powerful methods. More precisely, we propose a language to formally express system requirements and interpret verification results so that system designers (DSML end-users) avoid the burden of learning some formal verification technologies. Formal verification is achieved through translational semantics. This work is based on a metamodeling pattern for executable DSML that favors the definition of generative tools and thus eases the integration of tools for new DSMLs.

This works was funded by the french Ministry of Industry through the ITEA2 project OPEES and the french ANR project GEMOC.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Merilinna, J., Pärssinen, J.: Verification and validation in the context of domain-specific modelling. In: Proceedings of the 10th Workshop on Domain-Specific Modeling, ser. DSM 2010, pp. 9:1–9:6. ACM, New York (2010), http://doi.acm.org/10.1145/2060329.2060351

  2. Harel, D., Rumpe, B.: Meaningful Modeling: What’s the Semantics of “Semantics”? Computer 37(10), 64–72 (2004)

    Article  Google Scholar 

  3. Combemale, B., Crégut, X., Pantel, M.: A Design Pattern to Build Executable DSMLs and associated V&V tools (short paper). In: Asia-Pacific Software Engineering Conference (APSEC), Hong Kong, China (2012)

    Google Scholar 

  4. Ziemann, P., Gogolla, M.: An Extension of OCL with Temporal Logic. In: Critical Systems Development with UML – Proceedings of the UML 2002 Workshop, vol. TUM-I0208, pp. 53–62 (September 2002)

    Google Scholar 

  5. Software & Systems Process Engineering Metamodel (SPEM) 2.0. Object Management Group, Inc. (October 2007)

    Google Scholar 

  6. Berthomieu, B., Bodeveix, J.-P., Filali, M., Farail, P., Gaufillet, P., Garavel, H., Lang, F.: Fiacre: an Intermediate Language for Model Verification in the TopCased Environment. In: ERTS 2008 (January 2008)

    Google Scholar 

  7. Combemale, B., Crégut, X., Giacometti, J.-P., Michel, P., Pantel, M.: Introducing Simulation and Model Animation in the MDE TopCased Toolkit. In: Proceedings of the 4th European Congress Embedded Real Time Software (ERTS), Toulouse, France (January 2008)

    Google Scholar 

  8. Farail, P., Gaufillet, P., Canals, A., Camus, C.L., Sciamma, D., Michel, P., Crégut, X., Pantel, M.: The TopCased project: a toolkit in open source for critical aeronautic systems design. In: Embedded Real Time Software (ERTS), Toulouse, France (January 2006)

    Google Scholar 

  9. Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA – construction of abstract state spaces for Petri nets and time Petri nets. Int. Journal of Production Research 42(14), 2741–2756 (2004)

    Article  MATH  Google Scholar 

  10. Garavel, H., Lang, F., Mateescu, R., Serwe, W.: Cadp 2010: A toolbox for the construction and analysis of distributed processes. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 372–387. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  11. Correa, T., Becker, L., Farines, J.-M., Bodeveix, J.-P., Filali, M., Vernadat, F.: Supporting the Design of Safety Critical Systems Using AADL. In: 2010 15th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), pp. 331–336 (March 2010)

    Google Scholar 

  12. Farines, J.-M., De Queiroz, M.H., De Rocha, V., Carpes, A.M., Vernadat, F., Crégut, X.: A model-driven engineering approach to formal verification of PLC programs (regular paper). In: Emerging Technologies and Factory Automation (ETFA), Toulouse, France, pp. 1–8. IEEE (2011)

    Google Scholar 

  13. Jouault, F., Kurtev, I.: Transforming Models with ATL. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 128–138. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  14. Eclipse, Acceleo (2012), http://www.eclipse.org/acceleo/

  15. Abid, N., Dal-Zilio, S., Botlan, D.L.: A verified approach for checking real-time specification patterns. CoRR, vol. abs/1301.7531 (2013)

    Google Scholar 

  16. Zalila, F., Crégut, X., Pantel, M.: Verification results feedback for Fiacre intermediate language. In: Confrence en Ingnierie du Logiciel, CIEL (June 2012), http://gpl2012.irisa.fr/?q=node/31

  17. Abid, N., Dal Zilio, S.: Real-time Extensions for the Fiacre modeling language (2010), http://automata.rwth--aachen.de/movep2010/index.php?page=about , http://hal.archives-ouvertes.fr/hal-00593958

  18. Zalila, F., Crégut, X., Pantel, M.: Leveraging formal verification tools for DSML users: a process modeling case study. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012, Part II. LNCS, vol. 7610, pp. 329–343. Springer, Heidelberg (2012), http://hal.archives-ouvertes.fr/hal-00720917

    Chapter  Google Scholar 

  19. Jouault, F.: Loosely coupled traceability for ATLl. In: Proceedings of the European Conference on Model Driven Architecture (ECMDA) Workshop on Traceability (2005)

    Google Scholar 

  20. Chen, X., Hsieh, H., Balarin, F.: Verification approach of metropolis design framework for embedded systems. International Journal of Parallel Programming 34(1), 3–27 (2006)

    Article  MATH  Google Scholar 

  21. Barber, K.S., Graser, T., Holt, J.: Providing early feedback in the development cycle through automated application of model checking to software architectures. In: Proceedings of the 16th IEEE international conference on ASE 2001, Washington, DC, USA (2001)

    Google Scholar 

  22. Hegedüs, Á., Bergmann, G., Ráth, I., Varró, D.: Back-annotation of simulation traces with change-driven model transformations. In: SEFM 2010, pp. 145–155 (2010)

    Google Scholar 

  23. Combemale, B., Gonnord, L., Rusu, V.: A generic tool for tracing executions back to a dSML’s operational semantics. In: France, R.B., Kuester, J.M., Bordbar, B., Paige, R.F. (eds.) ECMFA 2011. LNCS, vol. 6698, pp. 35–51. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIT, Université de Toulouse, France

    Faiez Zalila, Xavier Crégut & Marc Pantel

Authors
  1. Faiez Zalila
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Xavier Crégut
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Marc Pantel
    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

Zalila, F., Crégut, X., Pantel, M. (2013). Formal Verification Integration Approach for DSML. 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_21

Download citation

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

  • 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