References of "Gammaitoni, Loïc 50001821"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailEnabling Value Co-Creation in Customer Journeys with VIVA
Razo-Zapata, Iván; Chew, Eng; Ma, Qin UL et al

in Joint International Conference of Service Science and Innovation and Serviceology (2018)

Detailed reference viewed: 16 (2 UL)
Full Text
See detailOn the Use of Alloy in Engineering Domain Specific Modeling Languages
Gammaitoni, Loïc UL

Doctoral thesis (2017)

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 ... [more ▼]

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. [less ▲]

Detailed reference viewed: 138 (16 UL)
Full Text
Peer Reviewed
See detailAgile Validation of Model Transformations using Compound F-Alloy Specifications
Gammaitoni, Loïc UL; Kelsen, Pierre UL; Ma, Qin

in Science of Computer Programming (2017)

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The ... [more ▼]

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The relational logic based specification language Alloy and its accompanying tool the Alloy Analyzer have been used in the past to validate properties of model transformations. However Alloy based analysis of transformations suffers from several limitations. On one hand, it is time consuming and does not scale well. On the other hand, the reliance on Alloy, being a formal method, prevents the effective involvement of domain experts in the validation process which is crucial for pinpointing domain pertinent errors. Those limitations are even more severe when it comes to transformations whose input and/or output are themselves transformations (called compound transformations) because they are inherently more complex. To tackle the performance and scalability limitations, in previous work, we proposed an Alloy-based Domain Specific Language (DSL), called F-Alloy, that is tailored for model transformation specifications. Instead of pure analysis based validation, F-Alloy speeds up the validation of model transformations by applying a hybrid strategy that combines analysis with interpretation. In this paper, we formalize the notion of “hybrid analysis” and further extended it to also support efficient validation of compound transformations. To enable the effective involvement of domain experts in the validation process, we propose in this paper a new approach to model transformation validation, called Visualization-Based Validation (briefly VBV). Following VBV, representative instances of a to-be-validated model transformation are automatically generated by hybrid analysis and shown to domain experts for feedback in a visual notation that they are familiar with. We prescribe a process to guide the application of VBV to model transformations and illustrate it with a benchmark model transformation. [less ▲]

Detailed reference viewed: 72 (4 UL)
Full Text
Peer Reviewed
See detailF-Alloy: a relational model transformation language based on Alloy
Gammaitoni, Loïc UL; Kelsen, Pierre UL

in Software & Systems Modeling (2017)

Model transformations are one of the core artifacts of a model-driven engineering approach. The relational logic language Alloy has been used in the past to verify properties of model transformations. In ... [more ▼]

Model transformations are one of the core artifacts of a model-driven engineering approach. The relational logic language Alloy has been used in the past to verify properties of model transformations. In this paper we introduce the concept of functional Alloy modules. In essence a functional Alloy module can be viewed as an Alloy module representing a model transformation. We describe a sublanguage of Alloy called F-Alloy specifically designed to concisely specify functional Alloy modules. The restrictions on F-Alloy’s syntax are meant to allow efficient execution of the specified transformation, without the use of backtracking, by an adapted interpretation algorithm. F-Alloy’s semantics is given in this paper as a direct translation to Alloy; hence, F-Alloy specifications are also analyzable using the powerful automatic analysis features of Alloy. [less ▲]

Detailed reference viewed: 62 (10 UL)
Full Text
Peer Reviewed
See detailRPSL meets lightning: A model-based approach to design space exploration of robot perception systems
Gammaitoni, Loïc UL; Hochgeschwender, Nico UL

in RPSL meets lightning: A model-based approach to design space exploration of robot perception systems (2016)

The design space of a robotic application defines at a meta level what are all of its possible implementations. Those possibilities are called design alternatives and differ on many different aspects, one ... [more ▼]

The design space of a robotic application defines at a meta level what are all of its possible implementations. Those possibilities are called design alternatives and differ on many different aspects, one being preferred to the other depending on how, where, when or what the application should do. Design Space Exploration (DSE) is the process of reviewing those design alternatives, prior to their implementation, with intention to verify that the set of all design alternatives to be implemented covers all the possible scenarios in which the application is to be executed. In this paper we address two challenges related to DSE, namely, (1) the formal definitions of design spaces, a non-trivial task due to the many dimensions to be taken into consideration, and (2) the automatisation of DSE, that is, enabling a domain expert to review design alternatives corresponding to a given design space effortlessly. In this paper, we address those challenges in the context of robot perception software systems by combining two already existing technologies, namely RPSL for the specification of robot perception system's design spaces and Lightning, a language workbench that we use to formalise RPSL and obtain, from RPSL specifications, corresponding design alternatives. [less ▲]

Detailed reference viewed: 61 (7 UL)
Full Text
Peer Reviewed
See detailAgile Validation of Higher Order Transformations Using F-Alloy
Gammaitoni, Loïc UL; Kelsen, Pierre UL; Ma, Qin

in Agile Validation of Higher Order Transformations Using F-Alloy (2016)

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The ... [more ▼]

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The relational logic based specification language Alloy and its accompanying tool the Alloy Analyzer have been used in the past to validate properties of model transformations. However Alloy based analysis of transformations suffers from time complexity and scalability issues. The problem becomes even more severe when it comes to higher order transformations that are inherently more complex. In previous work, we proposed a sub-language of Alloy, called F-Alloy, that is tailored for model transformation specifications. Instead of pure analysis based validation, F-Alloy speeds up the validation of model transformations by applying a hybrid strategy that combines analysis with interpretation. In this paper, we show how the F-Alloy approach can be extended to also support efficient validation of higher order transformations. [less ▲]

Detailed reference viewed: 84 (18 UL)
Full Text
Peer Reviewed
See detailDesigning Languages using Lightning
Gammaitoni, Loïc UL; Kelsen, Pierre UL; Glodt, Christian UL

in Proceedings of the 2015 ACM SIGPLAN International Conference on Software Language Engineering (2015)

Modelling languages are defined by specifying their abstract syntax, concrete syntax and semantics. In the Lightning tool the definition of all these language components is based on the lightweight formal ... [more ▼]

Modelling languages are defined by specifying their abstract syntax, concrete syntax and semantics. In the Lightning tool the definition of all these language components is based on the lightweight formal language Alloy. Lightning makes use of the powerful automatic analysis features of Alloy to allow language designers to develop and validate the definition of a modelling language in an incremental fashion. By providing immediate visual feedback, it allows errors in the language definition to be quickly identified and corrected. Furthermore Lightning introduces a novel interpretation mechanism that allows efficient execution of transformations used in the language definition. We illustrate the use of the tool on the language of structured business processes. [less ▲]

Detailed reference viewed: 256 (19 UL)
Full Text
Peer Reviewed
See detailF-Alloy: An Alloy Based Model Transformation Language
Gammaitoni, Loïc UL; Kelsen, Pierre UL

in Theory and Practice of Model Transformations (2015)

Model transformations are one of the core artifacts of a model-driven engineering approach. The relational logic language Alloy has been used in the past to verify properties of model transformations. In ... [more ▼]

Model transformations are one of the core artifacts of a model-driven engineering approach. The relational logic language Alloy has been used in the past to verify properties of model transformations. In this paper we introduce the concept of functional Alloy modules. In essence a functional Alloy module can be viewed as an Alloy module representing a model transformation. We describe a sublanguage of Alloy called F-Alloy that allows the specification of functional Alloy modules. Modules in F-Alloy are analysable using the powerful automatic analysis features of Alloy but can also be interpreted efficiently without the use of backtracking. [less ▲]

Detailed reference viewed: 192 (13 UL)
Full Text
Peer Reviewed
See detailVerifying Modelling Languages using Lightning: a Case Study
Gammaitoni, Loïc UL; Kelsen, Pierre UL; Mathey, Fabien

in MoDeVVa 2014: Model-Driven Engineering, Verification and Validation (2014)

The formal language Alloy was developed to provide fully automatic analysis of software designs. By providing immediate feedback to users it allows early detection of design errors. The main goal of the ... [more ▼]

The formal language Alloy was developed to provide fully automatic analysis of software designs. By providing immediate feedback to users it allows early detection of design errors. The main goal of the Lightning tool is to apply the power of Alloy's automatic analysis to the domain of software language engineering. The tool allows to represent abstract syntax, concrete syntax and semantics of a modelling language in Alloy. In this paper we describe the verification capabilities of Lightning with the help of a concrete modelling language, namely the language of structured business processes. [less ▲]

Detailed reference viewed: 169 (12 UL)
Full Text
Peer Reviewed
See detailDomain-Specific Visualization of Alloy Instances
Gammaitoni, Loïc UL; Kelsen, Pierre UL

in 4th International ABZ 2014 Conference (2014)

Detailed reference viewed: 197 (17 UL)
Full Text
Peer Reviewed
See detailThe paradoxes of permission an action based solution
Gabbay, Dov M. UL; Gammaitoni, Loïc UL; Sun, Xin UL

in Journal of Applied Logic (2014), 12(2), 179191

The aim of this article is to construct a deontic logic in which the free choice postulate allow (Ross, 1941) [11] would be consistent and all the implausible result mentioned in (Hanson, in press) [5 ... [more ▼]

The aim of this article is to construct a deontic logic in which the free choice postulate allow (Ross, 1941) [11] would be consistent and all the implausible result mentioned in (Hanson, in press) [5] will be blocked. To achieve this we first developed a new theory of action. Then we build a new deontic logic in which the deontic action operator and the deontic proposition operator are explicitly distinguished. [less ▲]

Detailed reference viewed: 54 (14 UL)
Full Text
See detailFunctional Alloy Modules
Gammaitoni, Loïc UL; Kelsen, Pierre UL

Report (2014)

The Alloy language was developed as a lightweight modelling language that allows fully automatic analysis of software design models via SAT solving. The practical application of this type of analysis is ... [more ▼]

The Alloy language was developed as a lightweight modelling language that allows fully automatic analysis of software design models via SAT solving. The practical application of this type of analysis is hampered by two limitations: first, the analysis itself can become quite time consuming when the scopes become even moderately large; second, determining minimal scopes for the entity types (limiting the number of entities of each type) to achieve better running times is itself a non-trivial problem. In this paper we show that for the special case of Alloy modules specifying transformations we may be able to circumvent these limitations. We define the corresponding notion of functional module and define precise conditions under which such functional modules can be efficiently interpreted rather than analysed via SAT solving and we also explain how interpretation of functional Alloy modules can be seamlessly integrated with the SAT-based analysis of other modules. We provide evidence that for complex transformations interpreting functional modules may result in significant time savings. [less ▲]

Detailed reference viewed: 139 (48 UL)