Search

Model transformations play a central role in model-driven software development. Hence, logical unsafe model transformation can result in erroneous systems. Still, most model transformations are written in languages that do not provide built-in safeness guarantees.We present a new technique to construct tool support for domain-specific languages (DSLs) inside the interactive theorem prover environment Isabelle. Our approach is based on modeling the DSL formally in higher-order logic (HOL), modeling the API of Isabelle inside it, and defining the transformation between these two. Reflection via the powerful code generators yields code that can be integrated as extension into Isabelle and its user interface. Moreover, we use code generation to produce tactic code which is bound to appropriate command-level syntax.Our approach ensures the logical safeness (conservativity) of the theorem prover extension and, thus, provides a certified tool for the DSL in all aspects: the deductive capacities of theorem prover, code generation, and IDE support. We demonstrate our approach by extending Isabelle/HOL with support for UML/OCL and, more generally, providing support for a formal object-oriented modeling method.

International audience; UML/OCL is perceived as the de-facto standard for specifyingobject-oriented models in general and data models in particular. Sincerecently, all data types of UML/OCL comprise two different exceptionelements: invalid ("bottom" in semantics terminology) and null (for"non-existing element"). This has far-reaching consequences on boththe logical and algebraic properties of OCL expressions as well as thepath expressions over object-oriented data structures, i.e., classmodels.In this paper, we present a formal semantics for object-oriented datamodels in which all data types and, thus, all class attributes andpath expressions, support invalid and null. Based on this formalsemantics, we present a set of OCL test cases that can be used forevaluating the support of null and invalid in OCL tools.

International audience; We show how modern proof environments comprising code generators andreflection facilities can be used for the effective construction of atool for OCL. For this end, we define a UML/OCL meta-model in HOL, ameta-model for Isabelle/HOL in HOL, and a compiling function betweenthem over the vocabulary of the libraries provided by FeatherweightOCL. We use the code generator of Isabelle to generate executable codefor the compiler, which is bound to a USE tool-like syntax integratedin Isabelle/Featherweight OCL. It generates for an arbitrary classmodel an object-oriented datatype theory and proves the relevantproperties for casts, type-tests, constructors and selectorsautomatically.

International audience; Modeling started out with UML and its precursors as a graphical notation. Such visual representations enable direct intuitive capturing of reality, but some of their features are difficult to formalize and lack the level of precision required to create complete and unambiguous specifications. Limitations of the graphical notations encouraged the development of text-based modeling languages that either integrate with or replace graphical notations for modeling. Typical examples of such languages are OCL, textual MOF, Epsilon, and Alloy. Textual modeling languages have their roots in formal language paradigms like logic, programming and databases. The goal of this workshop is to create a forum where researchers and practitioners interested in building models using OCL or other kinds of textual languages can directly interact, report advances, share results, identify tools for language development, and discuss appropriate standards. In particular, the workshop will encourage discussions for achieving synergy from different modeling language concepts and modeling language use. The close interaction will enable researchers and practitioners to identify common interests and options for potential cooperation.