Tool Paper: A Lightweight Formal Encoding of a Constraint Language for DSMLs

Arnaud Dieumegard (1, 2) , Marc Pantel (1, 2) , Guillaume Babin (1) , Martin Carton (1)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 Toulouse INP - Institut National Polytechnique (Toulouse)

Domain Specific Modeling Languages (dsmls) plays a key role in the development of Safety Critical Systems to model system requirements and implementation. They often need to integrate property and query sub-languages. As a standardized modeling language, ocl can play a key role in their definition as they can rely both on its concepts and textual syntax which are well known in the Model Driven Engineering community. For example, most dsmls are defined using mof for their abstract syntax and ocl for their static semantics as a metamodeling dsml. OCLinEcore in the Eclipse platform is an example of such a metamodeling dsml integrating ocl as a language component in order to benefit from its property and query facilities. dsmls for Safety Critical Systems usually provide formal model verification activities for checking models completeness or consistency, and implementation correctness with respect to requirements. This contribution describes a framework to ease the definition of such formal verification tools by relying on a common translation from a subset of ocl to the Why3 verification toolset. This subset was selected to ease efficient automated verification. This framework is illustrated using a block specification language for data flow languages where a subset of ocl is used as a component language.

Mots clés: DSMLs

Domaines: Génie logiciel [cs.SE]; Systèmes embarqués; Cryptographie et sécurité [cs.CR]; Interface homme-machine [cs.HC]; Architectures Matérielles [cs.AR]; Modélisation et simulation

Arnaud Dieumegard, Marc Pantel, Guillaume Babin, Martin Carton. Tool Paper: A Lightweight Formal Encoding of a Constraint Language for DSMLs. 15th International Workshop on OCL and Textual Modeling Workshop at the MODELS conference (OCL-TM 2015) co-located with 18th International Conference on Model Driven Engineering Languages and Systems, Sep 2015, Ottawa, Canada. pp. 89-104. ⟨hal-01316816⟩