Abstract
Formal methods are increasingly used in software engineering. They offer a formal frame that guarentees the correctness of developments. However, they use complex notations that might be difficult to understand for unaccustomed users. It thus becomes interesting to formally specify the core components of a language, implement a provably correct development, and manipulate its components in a graphical/textual editor.
This contribution constitutes a first step towards using Model Driven Engineering (MDE) technology in an interactive proof development. It presents a transformation process from functional data structures, commonly used in proof assistants, to Class diagrams in Ecore. To perform the transformation we use an MDE-based methodology. The resulting metamodels from the transformation process are used to generate textual or graphical editors for domain specific languages (DSLs) using tools provided by the Eclipse enviornment. To illustrate this approach we use as example a simple DSL description. It respresents a Java-like language enriched with timing annotations.
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.
References
Alanen, M., Porres, I.: A relation between context-free grammars and meta object facility metamodels. Tech. rep., Turku Centre for Computer Science (TUCS) (March 2003), http://www.cis.uab.edu/courses/cs593/spring2010/TR606.pdf
Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: A Challenging Model Transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436–450. Springer, Heidelberg (2007)
Baklanova, N., Strecker, M., Féraud, L.: Resource Sharing Conflicts Checking in Multithreaded Java Programs. In: Informal Proceedings FAC 2012 (April 2012)
Bézivin, J.: Model Driven Engineering: An Emerging Technical Space. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 36–64. Springer, Heidelberg (2006), https://www.uni-koblenz.de/~laemmel/gttse/2005/pdfs/41430036.pdf
Budinsky, F., Brodsky, S.A., Merks, E.: Eclipse Modeling Framework. Pearson Education (2003)
Coq Development Team: The Coq proof assistant reference manual. version 8.31 (2010), http://coq.inria.fr/refman/ , http://coq.inria.fr/refman/
Delahaye, D., Étienne, J.F., Viguié Donzeau-Gouge, V.: A Formal and Sound Transformation from Focal to UML: An Application to Airport Security Regulations. In: UML and Formal Methods (UML&FM), vol. 4, pp. 267–274 (2008), http://cedric.cnam.fr/~delahaye/?page=publis
van Deursen, A., Klint, P., Visser, J.: Domain-specific languages: An annotated bibliography. SIGPLAN Notices 35(6), 26–36 (2000)
Eclipse Community: Tutorials and documentation for Xtext 2.0 (2011), http://www.eclipse.org/Xtext/documentation/
Ehrig, K., Ermel, C., Hänsgen, S., Taentzer, G.: Generation of visual editors as Eclipse plugins. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering, ASE 2005, pp. 134–143. ACM, New York (2005), http://doi.acm.org/10.1145/1101908.1101930
France, R.B., Evans, A., Lano, K., Rumpe, B.: The UML as a formal modeling notation. Computer Standards & Interfaces 19(7), 325–334 (1998)
Gronback, R.C.: Eclipse Modeling Project: A Domain-Specific Language (DSL) Toolkit. Addison-Wesley, Upper Saddle River (2009)
Idani, A.: UML Models Engineering from Static and Dynamic Aspects of Formal Specifications. In: Halpin, T., Krogstie, J., Nurcan, S., Proper, E., Schmidt, R., Soffer, P., Ukor, R. (eds.) BPMDS 2009 and EMMSAD 2009. LNBIP, vol. 29, pp. 237–250. Springer, Heidelberg (2009)
Idani, A., Boulanger, J.L., Philippe, L.: A generic process and its tool support towards combining UML and B for safety critical systems. In: Hu, G. (ed.) CAINE, pp. 185–192. ISCA (2007)
Kleppe, A.G., Warmer, J., Bast, W.: MDA Explained: The Model Driven Architecture: Practice and Promise. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)
de Lara, J., Vangheluwe, H.: Using AToM3 as a meta-case tool. In: Proceedings of the 4th International Conference on Enterprise Information Systems (ICEIS), Ciudad Real, Spain, pp. 642–649 (April 2002), http://www.cs.mcgill.ca/~hv/publications/02.ICEIS.MCASE.pdf
Leroy, X., Doligez, D., Frisch, A., Garrigue, J., Rémy, D., Vouillon, J.: The OCaml system release 3.12. documentation and user’s manual (July 2011), http://caml.inria.fr/pub/docs/manual-ocaml/index.html
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002), http://isabelle.in.tum.de
Odersky, M., Altherr, P., Cremet, V., Emir, B., Maneth, S., Micheloud, S., Mihaylov, N., Schinz, M., Stenman, E., Zenger, M.: An Overview of the Scala Programming Language. Tech. Rep. IC/2004/64, EPFL Lausanne, Switzerland (2007)
OMG: Meta Object Facility (MOF) Core v. 2.0 Document (2006), http://www.omg.org
Peyton-Jones, S.: Haskell 98 language and libraries: the revised report. Cambridge University Press, Cambridge (2003), http://www.worldcat.org/isbn/9780521826143
Selic, B.: The pragmatics of model-driven development. IEEE Software 20(5), 19–25 (2003)
Shah, S.M.A., Anastasakis, K., Bordbar, B.: From UML to Alloy and Back Again. In: Ghosh, S. (ed.) MODELS 2009. LNCS, vol. 6002, pp. 158–171. Springer, Heidelberg (2010)
Steele, G.L.: Common LISP, 2nd edn. Digital Press (1990)
Wimmer, M., Kramler, G.: Bridging Grammarware and Modelware. In: Bruel, J.-M. (ed.) MoDELS 2005. LNCS, vol. 3844, pp. 159–168. Springer, Heidelberg (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Djeddai, S., Mezghiche, M., Strecker, M. (2013). Combining Verification and MDE Illustrated by a Formal Java Development. In: Ermolayev, V., Mayr, H.C., Nikitchenko, M., Spivakovsky, A., Zholtkevych, G. (eds) ICT in Education, Research, and Industrial Applications. ICTERI 2012. Communications in Computer and Information Science, vol 347. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-35737-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-35737-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-35736-7
Online ISBN: 978-3-642-35737-4
eBook Packages: Computer ScienceComputer Science (R0)