Doctoral thesis (Dissertations and theses)
On the Use of Alloy in Engineering Domain Specific Modeling Languages
Gammaitoni, Loïc
2017
 

Files


Full Text
thesis.pdf
Author preprint (3.54 MB)
Download

All documents in ORBilu are protected by a user license.

Send to



Details



Keywords :
DSL; DSML; F-Alloy; Alloy; model transformation; Lightning; Language Workbench; RPSL; endogenous; exogenous; formal methods; analysis; interpretation; coumpound; visualization; validation
Abstract :
[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.
Disciplines :
Computer science
Author, co-author :
Gammaitoni, Loïc ;  University of Luxembourg > Faculty of Science, Technology and Communication (FSTC) > Computer Science and Communications Research Unit (CSC)
Language :
English
Title :
On the Use of Alloy in Engineering Domain Specific Modeling Languages
Defense date :
16 October 2017
Institution :
Unilu - University of Luxembourg, Luxembourg
Degree :
Docteur en Informatique
Promotor :
President :
Jury member :
Combemale, Benoit
Cuhna, Alcino
Navet, Nicolas 
Focus Area :
Security, Reliability and Trust
Available on ORBilu :
since 29 November 2017

Statistics


Number of views
251 (22 by Unilu)
Number of downloads
343 (14 by Unilu)

Bibliography


Similar publications



Contact ORBilu