Reference : On the Use of Alloy in Engineering Domain Specific Modeling Languages
Dissertations and theses : Doctoral thesis
Engineering, computing & technology : Computer science
Security, Reliability and Trust
On the Use of Alloy in Engineering Domain Specific Modeling Languages
Gammaitoni, Loïc mailto [University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC) >]
University of Luxembourg, ​​Luxembourg
Docteur en Informatique
Kelsen, Pierre mailto
Sorger, Ulrich mailto
Combemale, Benoit mailto
Cuhna, Alcino mailto
Navet, Nicolas mailto
[en] DSL ; DSML ; F-Alloy ; Alloy ; model transformation ; Lightning ; Language Workbench ; RPSL ; endogenous ; exogenous ; formal methods ; analysis ; interpretation ; coumpound ; visualization ; validation
[en] Domain Specific Modeling Languages (DSMLs) tend to play a central role in modern design processes as they enable the effective involvement of domain experts by focusing on a particular problem domain while abstracting away technical details. In this thesis, we investigate the specification of DSMLs with a particular focus on domain expert driven validation. Mainly, we are interested in developing Alloy-based approaches, allowing the definition of specifications from which instances can be generated and given to the domain experts for the sake of validation.

The work we present in this thesis can be divided into three parts:

The first part concerns the definition and execution of model transformations defined in Alloy. While Alloy analysis can be used as an execution engine for model transformations, the analysis process is time consuming. Model transformations playing a central role in DSML definitions, the development of a new model transformation language, named F-Alloy, retaining the benefits of Alloy with the added property of being efficiently computable was necessary.

The second part focuses on validation. In that domain, our first contribution is a novel approach to the validation of model transformations called Visualization-Based Validation (VBV). VBV relies on the review by domain experts of intuitive depictions of model transformation traces to validate model transformation specifications. The whole process is made efficient by the usage of hybrid analysis, a combination of Alloy analysis and F-Alloy interpretation, allowing to reduce the time needed to analyze model transformations to the time needed to analyze its source.
Our second contribution in the validation area is the definition of an Alloy-based approach to the specification and validation of DSMLs and of a design process defining how DSMLs can be validated using Alloy analysis at each iteration of the process. More precisely, we present how the abstract syntax, concrete syntax and operational semantics of a DSML can be defined using Alloy and F-Alloy, and show that the validation of a DSML' s abstract syntax and semantics benefits from the application of its concrete syntax.

The third and last part aims at bringing those contributions to the practical world. To achieve this we developed a tool named Lightning implementing the aforementioned contributions. This tool, which belongs to the category of language workbenches, has been successfully used in an inter-disciplinary collaboration to define the Robot Perception System Language (RPSL). Based on this definition of RPSL, a framework has been developed to allow the execution of so called design space explorations. This framework represents a successful application of our approach to the real world problem of having RPSL specifications validated by experts in robotics.

File(s) associated to this reference

Fulltext file(s):

Open access
thesis.pdfAuthor preprint3.46 MBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.