OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

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

Dieumegard, Arnaud and Pantel, Marc and Babin, Guillaume and Carton, Martin Tool Paper: A Lightweight Formal Encoding of a Constraint Language for DSMLs. (2015) In: 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, 27 September 2015 - 2 October 2015 (Ottawa, Canada).

[img]
Preview
(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
334kB

Official URL: https://ocl2015.lri.fr/OCL_2015_paper_1111_1430.pdf

Abstract

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.

Item Type:Conference or Workshop Item (Paper)
HAL Id:hal-01316816
Audience (conference):International conference proceedings
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - INPT (FRANCE)
French research institutions > Centre National de la Recherche Scientifique - CNRS (FRANCE)
Université de Toulouse > Université Paul Sabatier-Toulouse III - UPS (FRANCE)
Université de Toulouse > Université Toulouse - Jean Jaurès - UT2J (FRANCE)
Université de Toulouse > Université de Toulouse I-Sciences Sociales - UT1 (FRANCE)
Laboratory name:
Statistics:download
Deposited By: IRIT IRIT
Deposited On:06 Apr 2016 13:41

Repository Staff Only: item control page