Results 1-20 of 32.
((uid:50002081))

Bookmark and Share    
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: 55 (3 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: 32 (6 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: 71 (18 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: 155 (12 UL)
Full Text
Peer Reviewed
See detailBusiness Process Regulatory Compliance is Hard
Colombo Tosatto, Silvano UL; Kelsen, Pierre UL; Governatori, Guido

in IEEE Transactions on Services Computing (2015), 8(6), 958-970

Verifying whether a business process is compliant with a regulatory framework is a difficult task. In the present paper we prove the hardness of the business process regulatory compliance problem by ... [more ▼]

Verifying whether a business process is compliant with a regulatory framework is a difficult task. In the present paper we prove the hardness of the business process regulatory compliance problem by taking into account a sub-problem of the general problem. This limited problem allows to verify only the compliance of structured processes with respect to a regulatory framework composed of a set of conditional obligations including a deadline. Experimental evidence from existing studies shows that compliance is a difficult task. In this paper, despite considering a sub-problem of the general problem, we provide some theoretical evidence of the difficulty of the task. In particular we show that the source of the complexity lies in the core language of verifying conditional obligations with a deadline. We prove that for this simplified case verifying partial compliance belongs to the class of NP-complete problems, and verifying full compliance belongs to the class of coNP-complete problems. Thus by proving the difficulty of a simplified compliance problem we prove that the general problem of verifying business process regulatory compliance is hard. [less ▲]

Detailed reference viewed: 74 (18 UL)
Full Text
Peer Reviewed
See detailA generic model decomposition technique and its application to the Eclipse modeling framework
Ma, Qin UL; Kelsen, Pierre UL; Glodt, Christian UL

in Software & Systems Modeling (2015), 14(2), 921-952

Model-driven software development aims at easing the process of software development by using models as primary artifacts. Although less complex than the real systems they are based on, models tend to be ... [more ▼]

Model-driven software development aims at easing the process of software development by using models as primary artifacts. Although less complex than the real systems they are based on, models tend to be complex nevertheless, thus making the task of handling them non-trivial in many cases. In this paper we propose a generic model decomposition technique to facilitate model management by decomposing complex models into smaller sub-models that conform to the same metamodel as the original model. The technique is based upon a formal foundation that consists of a formal capturing of the concepts of models, metamodels, and model conformance; a formal constraint language based on EssentialOCL; and a set of formally proved properties of the technique. We organize the decomposed sub-models in a mathematical structure as a lattice, and design a linear-time algorithm for constructing this decomposition. The generic model decomposition technique is applied to the Eclipse Modeling Framework (EMF) and the result is used to build a solution to a specific model comprehension problem of Ecore models based upon model pruning. We report two case studies of the model comprehension method: one in BPMN and the other in fUML. [less ▲]

Detailed reference viewed: 73 (24 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: 197 (15 UL)
Full Text
Peer Reviewed
See detailAlgorithms for tractable compliance problems
Colombo Tosatto, Silvano UL; Kelsen, Pierre UL; Ma, Qin UL et al

in Frontiers of Computer Science (2015), 9(1), 55-74

In general the problem of verifying whether a structured business process is compliant with a given set of regulations is NP-hard. The present paper focuses on identifying a tractable subset of this ... [more ▼]

In general the problem of verifying whether a structured business process is compliant with a given set of regulations is NP-hard. The present paper focuses on identifying a tractable subset of this problem, namely verifying whether a structured business process is compliant with a single global obligation. Global obligations are those whose validity spans for the entire execution of a business process. We identify two types of obligations: achievement and maintenance. In the present paper we firstly define an abstract framework capable to model the problem and secondly we define procedures and algorithms to deal with the compliance problem of checking the compliance of a structured business process with respect to a single global obligation. We show that the algorithms proposed in the paper run in polynomial time. [less ▲]

Detailed reference viewed: 81 (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: 134 (48 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: 166 (17 UL)
Full Text
Peer Reviewed
See detailDetecting Deontic Conflicts in Dynamic Settings
Colombo Tosatto, Silvano UL; Kelsen, Pierre UL; Governatori, Guido

in Cariani, Fabrizio; Grossi, Davide; Meheus, Joke (Eds.) et al Deontic Logic and Normative Systems 12th International Conference, DEON 2014, Ghent, Belgium, July 12-15, 2014. Proceedings (2014)

Regulations, through the use of obligations and permissions, are widely used in modern society to define acceptable behaviours. Thus it is indeed important that these regulations do not conflict with each ... [more ▼]

Regulations, through the use of obligations and permissions, are widely used in modern society to define acceptable behaviours. Thus it is indeed important that these regulations do not conflict with each other and contain contradicting obligations. In the present paper we focus on identifying conflicts between obligations in dynamic settings. We first show the need of an alternative semantics rather than the more classic modelled by standard deontic logic. Second we introduce a new semantics for the obligations capable of representing and reasoning about them in these dynamic settings, and lastly we use it to identify the necessary and sufficient conditions to identify conflicting obligations. [less ▲]

Detailed reference viewed: 39 (2 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: 140 (11 UL)
Full Text
Peer Reviewed
See detailCombining Models with Code: a Tale of Two Languages
Qin, Ma; Schmit, Sam; Glodt, Christian UL et al

in IEEE International Conference on Global Software Engineeering Workshops (2014)

In the pure model-driven view of software engineering, models are the sole artifacts to be created and maintained and executable source code is entirely generated from the models. However, due to the ... [more ▼]

In the pure model-driven view of software engineering, models are the sole artifacts to be created and maintained and executable source code is entirely generated from the models. However, due to the variety of modern platforms and the complexity of capturing them correctly in models, this vision has not yet been fully realized. In this paper, we propose an approach that allows combining high-level models with low-level code into an executable system. The approach is based on two modeling languages, one presenting a common abstraction of modeling and programming languages, and the other allowing to express the bridge between the model and code. We illustrate our approach using a running example of an invoicing system for which the business logic requirements are captured by an executable model and the requirements on the graphical user interface are directly mocked up using a GUI designer tool that generates Java code. [less ▲]

Detailed reference viewed: 51 (1 UL)
Full Text
Peer Reviewed
See detailTowards an Abstract Framework for Compliance
Colombo Tosatto, Silvano UL; Governatori, Guido; Kelsen, Pierre UL

in Bagheri, Ebrahim; Gasevic, Dragan; Halle, Sylvain (Eds.) et al Proceedings of the 17th IEEE International EDOC 2013 Conference Workshops, Vancouver, Canada, 9 September 2013. (2013, September 09)

The present paper aims at providing an abstract framework to define the regulatory compliance problem. In particular we show how the framework can be used to solve the problem of deciding whether a ... [more ▼]

The present paper aims at providing an abstract framework to define the regulatory compliance problem. In particular we show how the framework can be used to solve the problem of deciding whether a structured process is compliant with a single regulation, which is composed of a primary obligation and a chain of compensations. [less ▲]

Detailed reference viewed: 62 (8 UL)
Full Text
Peer Reviewed
See detailAlgorithms for Basic Compliance Problems
Colombo Tosatto, Silvano UL; El Kharbili, Marwane UL; Governatori, Guido et al

in 2nd International Workshop on Engineering Safety and Security Systems, ESSS 2013. (2013, March)

The present paper focuses on the problems of verifying compliance for global achievement and maintenance obligations. We first introduce the elements needed to identify and study compliance to these two ... [more ▼]

The present paper focuses on the problems of verifying compliance for global achievement and maintenance obligations. We first introduce the elements needed to identify and study compliance to these two classes of obligations in processes. Additionally, we define procedures and algorithms to efficiently deal with the identified compliance problem. We finally show that both algorithms proposed in the paper belong to the complexity class P. [less ▲]

Detailed reference viewed: 114 (13 UL)
Full Text
See detailVisual Modelling of and on Tangible User Interfaces
Tobias, Eric; Kelsen, Pierre UL

Report (2012)

The purpose of this thesis is to investigate the use and benefit of visual modelling languages (VMLs) in modelling on tangible user interfaces (TUIs), and modelling TUI applications. Three main research ... [more ▼]

The purpose of this thesis is to investigate the use and benefit of visual modelling languages (VMLs) in modelling on tangible user interfaces (TUIs), and modelling TUI applications. Three main research questions are asked: - Is it possible and practical to model an application or process using a TUI? - Which General-purpose VML (GPVML) performs best in modelling a VML scenario for use on TUI? - Is it realistic to use a GPVML to model complex TUI applications? To answer the first research question, a Business Process Model and Notation, version 2 (BPMN2), ideation scenario is used with a tangible widget toolkit prototype on a TUI table to evaluate the performance and obtain feedback from test candidates. The study showed that it is possible to model a process using a TUI and the test candidate feedback did not lead to the conclusion that the modelling was cumbersome or impractical. To find a suitable GPVML, the thesis explores and evaluates the current state of the art in VMLs for describing general problems. After gathering different VMLs, the thesis compares three languages using a simple scenario: the visual object constraint language (VOCL), augmented constraint diagrams (ACD), and the visual contract language (VCL). A weighted evaluation based on multiple quality criteria led to the conclusion that VCL is best suited to model TUI applications, answering the second research question. The thesis answers the third research question by using VCL to model a more complex and complete scenario of an ideation process, which is based on using a BPMN2 on a TUI. This is done to assess VCL's suitability to more complex problems and its maturity. The study concludes that VCL is not yet mature enough to enable its general applicability in a wide variety of settings. The three research questions were dressed with a hypothesis in mind: collaborative, novice friendly modelling environments are able to reduce the gap between stakeholders and software engineers during software projects, leading to a reduction of unrealistic expectations and an increase in the availability of domain knowledge. While the hypothesis is too broad to be proven by this thesis, the research questions answered here give some insights into how to approach it. [less ▲]

Detailed reference viewed: 99 (3 UL)
Full Text
Peer Reviewed
See detailModels within Models: Taming Model Complexity Using the Sub-model Lattice
Kelsen, Pierre UL; Ma, Qin UL; Glodt, Christian UL

in 14th International Conference on Fundamental Approaches to Software Engineering (FASE 2011) (2011)

Model-driven software development aims at easing the process of software development by using models as primary artifacts. Although less complex than the real systems they are based on, models tend to be ... [more ▼]

Model-driven software development aims at easing the process of software development by using models as primary artifacts. Although less complex than the real systems they are based on, models tend to be complex nevertheless, thus making the task of comprehending them non-trivial in many cases. In this paper we propose a technique for model comprehension based on decomposing models into sub-models that conform to the same metamodel as the original model. The main contributions of this paper are: a mathematical description of the structure of these sub-models as a lattice, a linear-time algorithm for constructing this decomposition and finally an application of our decomposition technique to model comprehension. [less ▲]

Detailed reference viewed: 69 (15 UL)
Full Text
Peer Reviewed
See detailBuilding VCL Models and Automatically Generating Z Specifications from Them
Amalio, Nuno UL; Glodt, Christian UL; Kelsen, Pierre UL

in Formal Methods - 17th International Symposium on Formal Methods (2011)

VCL is a visual and formal language for abstract specification of software systems. Its novelty lies in its capacity to describe predicates visually. This paper presents work-in-progress on a tool for VCL ... [more ▼]

VCL is a visual and formal language for abstract specification of software systems. Its novelty lies in its capacity to describe predicates visually. This paper presents work-in-progress on a tool for VCL; the tool version presented here supports the VCL notations of structural and assertion diagrams (a subset of the whole VCL suite), enabling the generation of Z specifications from them. [less ▲]

Detailed reference viewed: 37 (2 UL)
Full Text
Peer Reviewed
See detailAutomated Generation of Platform-Variant Applications from Platform-Independent Models via Templates
Amalio, Nuno UL; Glodt, Christian UL; Pinto, Frederico et al

in Electronic Notes in Theoretical Computer Science (2011), 279(3), 3-25

Model-driven development raises the level of abstraction so that software engineers can focus on design rather than implementation and platform-specific details. This paper presents a model-centric ... [more ▼]

Model-driven development raises the level of abstraction so that software engineers can focus on design rather than implementation and platform-specific details. This paper presents a model-centric approach to MDD, where platform code is generated from a platform-independent model describing platform-variant families of products. The generation is done via templates; the variation point lies in the alternative execution platforms. Our approach is based on EP, a formal executable modelling language, supplemented with OCL, and FTL, a formal language of templates. The paper illustrates the approach by generating applications from the same abstract model that run on both Googleâ Android and Apple iPhone mobile platforms. The paper contribution are: (a) it realises the MDD approach using formal languages, in particular the use of a formal language of templates and (b) it illustrates the approach by generating code for two distinct platforms. [less ▲]

Detailed reference viewed: 38 (1 UL)
Full Text
Peer Reviewed
See detailEnterprise Regulatory Compliance Modeling using CoReL: An illustrative Example
El Kharbili, Marwane UL; Ma, Qin UL; Kelsen, Pierre UL et al

in The 13th IEEE Conference on Commerce and Enterprise Computing, CEC 2011 (2011)

Regulatory compliance management is a critical and challenging task, especially in the context of Business Process Management. It requires a comprehensive framework for dealing with compliance ... [more ▼]

Regulatory compliance management is a critical and challenging task, especially in the context of Business Process Management. It requires a comprehensive framework for dealing with compliance requirements: elicitation, modeling, static and dynamic checking and reporting. We previously defined CoReL, a domain specific language for the domain of compliance decision-making. This paper shows how CoReL can be used to model compliance requirements using an illustrative example. In particular, we show how CoReL agnosticism of logical formalisms and coverage of enterprise business aspects leverages the task of compliance modeling to the business user level. [less ▲]

Detailed reference viewed: 41 (1 UL)