Technical Reports@CS

Bentley James Oakes, Levi Lúcio, Cláudio Gomes, and Hans Vangheluwe, "Expressive Symbolic-Execution Contract Proving for the DSLTrans Transformation Language", Computer Science, McGill University, Jan. 31, 2017, CS-TR-2017.1 Abstract
Abstract

The verification of model transformations is key for the adoption of model-driven engineering
in academic and industrial processes. In this work, we provide a verification technique for
our model transformation language DSLTrans, which is both confluent and terminating by
construction.

This technique proves structural pre-condition/ post-condition structural contracts for all
inputs to a transformation. This is achieved by creating path conditions for the transformation through a symbolic execution of the transformation’s rules. These path conditions then
represent all possible transformation executions through an abstraction relation.

In this work, we provide a detailed description of both the path condition construction and
contract proving techniques. As well, we provide arguments that our techniques are valid, such
that proving a contract on the finite set of path conditions for a transformation implies that
the contract holds on the infinite set of abstracted transformation executions.

Download Technical Report
Yentl Van Tendeloo and Hans Vangheluwe, "Explicit Type Instance Relations", School of Computer Science, McGill University, June 20, 2016, CS-TR-2016.12016.1 Abstract
Abstract

The basic building block for constructing a modelling tool architecture, is the relationship between a type and its instances. It is this relation which gives rise to the hierarchy that forms the foundation of the four-layer-architecture and to multi-level modelling. Only through the type/instance relation, a distinction is made between a model and its type model. This relation consists of two equally important components: instantiation and conformance. As both form the foundation of a (meta-)modelling tool, they are often hardcoded, both for conceptual and performance reasons. While this seems logical, it constrains users to the problems envisioned by the tool developers. It becomes necessary to alter models that are not a perfect fit for the provided framework, increasing accidental complexity. Incidentallly, minimizing accidental complexity is one of the core goals of Model Driven Engineering. In this report, we consider the limitations imposed by a hardcoded conformance relation. We also present our approach of explicitly modelling the conformance relation: users can chose which conformance to use, and gain insight in the semantics of the tool. We discuss the advantages of this approach, and how this was implemented in our tool: the Modelverse. An example is given where different notions of conformance are used for both structural and nominal subtyping.

Download Technical Report
Syed Ahmed, Muthucumaru Maheswaran, "Design and Challenges of a Lightweight Container-Based Architecture for Multi-Clouds", School of Computer Science, McGill University, Feb. 9, 2015, CS-TR-2015.2 Abstract
Abstract
Cloud computing is a major part of the modern computing landscape. Although cloud computing systems already offer many advantages, there is a need to interconnect them such that resources from one provider can be substituted for resources from another provider. For existing cloud providers such a marketplace offers many advantages and disadvantages. In this paper, we outline an architecture for creating an multi- cloud without the full cooperation of the participating cloud providers. Our multi-cloud architecture leverages several new technologies that have started gaining a foothold in the industry such as Linux containers and software defined networking. We present a detailed description of the architecture and explain the challenges that need to be addressed in realizing it. In particular, we want an multi-cloud that is lightweight as possible and does not create a significant compute, memory, or storage footprint by itself.
Download Technical Report
Omar Alam, Jörg Kienzle and Gunter Mussbacher, "Concern-Driven Software Development", School of Computer Science, McGill University, Jan. 26, 2015, CS-TR-2015.1 Abstract
Abstract
This paper describes the vision of Concern-Driven Development (CDD), a novel software development paradigm that extends model-driven engineering with best practices from reuse, advanced modularization techniques, goal modelling, and software product line research. CDD advocates the use of a three-part interface to describe units of reuse, i.e., concerns. The variation interface de- scribes required design decisions and their impact on high level system qualities, both explicitly expressed using feature models and goal models. The customization interface allows the chosen variation to be adapted to a specific reuse context, while the us- age interface defines how a customized concern may eventually be used. When a concern is reused, the modeller first uses the varia- tion interface to select the feature configuration that has the desired impact on stakeholder goals and system qualities, then adapts the concern to the context of the application under development with the help of the customization interface, and finally accesses the concern’s functionality through its usage interface. We argue that, if CDD is successfully adopted on a large scale, it will transform the software engineering discipline by enabling software engineers to specialize to a greater degree and hence align the practice of software engineering closer to what is done in other engineering disciplines.
Download Technical Report
Ken Vanherpen, Joachim Denil, Paul De Meulenaere, and Hans Vangheluwe, "Design-Space Exploration in Model Driven Engineering –An Initial Pattern Catalogue–", School of Computer Science, McGill University, Aug. 15, 2014, CS-TR-2014.4 Abstract
Abstract

A designer often has to evaluate alternative designs during the development of a system. A multitude of Design-Space Exploration (DSE) techniques exist in the literature. Integration of these techniques into the modelling paradigm is needed when a model-driven engineering approach is used for designing systems. To a greater or lesser extent, the integration of those different DSE techniques share characteristics with each other. Inspired by software design patterns, we introduce an initial pattern catalogue to categorise the embedding of different DSE techniques in an MDE context. We demonstrate their use by a literature survey and discuss the consequences of each pattern. Finally, we demonstrate the application of our initial pattern catalogue on two examples.

Download Technical Report
Bart Meyers and Romuald Deshayes and Levi Lucio and Eugene Syriani and Manuel Wimmer and Hans Vangheluwe, "The ProMoBox Approach to Language Modelling", School of Computer Science, McGill University, May 15, 2014, CS-TR-2014.3 Abstract
Abstract
The goal of Domain-Specific Language (DSL) engineering is to optimally support the tool-based construction of domain-specific languages and models. These tools should be suitable for use by domain experts rather than being accessible only by technical experts. Domain experts wish to design, document, analyse, simulate, optimise, and synthesise complex, software-intensive systems. The above goal implies that a DSL must combine a number of sub-languages, as not only the system-under-study, but also its input, output, properties, system state, and verification results (e.g., counter-example traces) need to be expressed in a domain-user-friendly way. Many current domain-specific modelling tools are coded in programming languages. This allows for extensive customisation, high expressiveness and performance, but lacks means for maintaining and extending the DSL. To overcome these drawbacks, an alternative approach models the DSL explicitly using meta-modelling and model transformations.Domain-specific modelling tools are then synthesized from these models. However, this approach requires, for each new language variant, the manual creation of each of the required sub-languages. Furthermore, these sub-languages and their specifications need to be kept consistent. The ProMoBox approach we propose aims to ease the specification of DSLs by generating the entire family of languages from a limited set of models (the ProMoBox), thus minimizing the effort to create and evolve a DSL and its sub-languages. Consistency is guaranteed by construction. This is done by generating meta-models, concrete syntax models and a precisely defined semantics for each language variant from an annotated meta-model and operational semantics model. We give a precise description of the ProMoBox modelling and generation process and demonstrate the approach by means of an elevator control DSL.
Bentley James Oakes, "Optimizing Simulink Models", School of Computer Science, McGill University, April 27, 2014, CS-TR-2014.5 Abstract
Abstract
The Simulink modelling tool is used to diagram and study cyber-physical systems. One advantage of modelling the systems in this way is that embeddable code can generated from the models directly. However, this process means that inefficiencies in the model may be propagated to the code. Code generation optimizations are available, but may lead to an unacceptable loss of traceability in determining which parts of the model were modified or removed during code generation. In our work, we focus on defining model-to-model optimizations. This means that the optimized model can be loaded back into Simulink for further development or analysis, improving traceability and allowing model specialization for different platforms. An analysis framework has been created, based on dataflow analysis from the compiler optimization domain. This allows fast and accurate definition of new optimizations. As well, an initial optimization classification was developed to aid in the discovery of new optimizations. At the present time, we have implemented three optimizations in our framework: constant folding, dead-block removal, and hierarchy flattening. These optimizations are intended to simplify the model and potentially increase model performance when simulated. Our framework allows us to communicate directly with a Simulink instance to import and export models, allowing us to test these optimizations on a number of sample Simulink models. In order to test the performance benefits of our optimizations, our experiments generated simulation code for the model before and after optimization. Examining the run-time of these simulations indicated that the constant folding optimization decreased the run-time on all applicable models when code generation optimizations were not used. This decrease in run-time is well above the fraction of a second that the analysis and transformation took for this optimization. Thus, a net gain in performance was obtained. Other optimizations did not show performance results, but did produce a simplified model, which is also desirable for a modeller.
Download Technical Report
Joachim Denil and Maris Jukss and Clark Verbrugge and Hans Vangheluwe, "Search-Based Model Optimization using Model Transformations", School of Computer Science, McGill University, Jan. 16, 2014, CS-TR-2014.2 Abstract
Abstract
With the advent of new and more complex software engineering problems and applications, synergies between Search-Based Software Engineering (SBSE) and Model-Driven Engineering (MDE) have been proposed. SBSE formulates the software engineering problem as a search-based optimization (SBO) problem. In Model-Driven Engineering, model transformation is the preferred technique to manipulate models. The challenge thus lies in adapting model transformations to tackle SBO tasks. In this paper we explore the inclusion of search directly in model transformations, without the need for an intermediate representation. We also investigate the feasibility and scalability of the approach on an industrial scale problem of resource allocation. We demonstrate that our solution is feasible and applicable to problems where representing the problem in a search amenable representation is time consuming, hard or even impossible.
Download Technical Report
Levi Lucio and Bentley James Oakes and Hans Vangheluwe, "A Technique for Symbolically Verifying Properties of Graph-Based Model Transformations", School of Computer Science, McGill University, Jan. 15, 2014, CS-TR-2014.1 Abstract
Abstract
Levi Lucio and Hans Vangheluwe, "Symbolic Execution for the Verification of Model Transformations", School of Computer Science, McGill University, April 15, 2013, CS-TR-2013.2 Abstract
Abstract
In this paper we present our implementation of a tool for proving properties of model transformations expressed in the DSLTrans language. The properties we are interested in regard relations between the structure of the in- put and output models. In particular the properties are implications of the form ‘if a structural relation between some elements of the source model holds, then another structural relation between some elements of the target model must also hold’. Our technique is transformation dependent but model independent, meaning the proofs we produce will hold for all executions of a given DSLTrans model transformation specification running on the potentially infinite instances of the transformation’s input metamodel. Our proof technique is based on 1) building the set of symbolic executions for a given DSLTrans transformation and 2) on exploring those symbolic executions to check whether the property holds. Due to the fact that DSLTrans transformations are both terminating and confluent by construction, we are able to build a finite set of symbolic executions by abstracting from the number of times the transformation’s rules match on concrete elements of input models. We explain how a set of symbolic executions and a proof is built in our tool by using (higher order) transformations developed with the T-Core framework. Furthermore we apply our tool to the proof of properties of an example transformation and present some scalability results for our approach.
Maris Jukss, Clark Verbrugge, Maged Elaasar, Hans Vangheluwe, "Scope in model transformations", School of Computer Science, McGill University, Jan. 17, 2013, CS-TR-2013.4 Abstract
Abstract
Levi Lucio, Moussa Amrani, Juergen Dingel, Leen Lambers, Rick Salay, Gehan Selim, Eugene Syriani, Manuel Wimmer, "Properties of Model Transformation Intents", School of Computer Science, McGill University, Jan. 16, 2013, CS-TR-2013.3 Abstract
Abstract
The notion of model transformation intent is proposed to capture the purpose of a transformation. A framework for the description of model transformation intents is defined which includes, for instance, a description of properties a model transformation has to satisfy to qualify as a suitable realization of an intent. Several common model transformation intents are identified and the framework is used to describe five of them in detail. A case study from the automotive industry is used to demonstrate the usefulness of the proposed framework for identifying crucial properties of model transformations with different intents and to illustrate the wide variety of model transformation intents that an industrial model-driven software development process typically en- compasses.
Joachim Denil, Gang Han, Magnus Persson, Paul De Meulenaere, Haibo Zeng, Xue Liu, Hans Vangheluwe, "Model-Driven Engineering Approaches to Design Space Exploration", School of Computer Science, McGill University, Jan. 15, 2013, CS-TR-2013.1 Abstract
Abstract
During the design and deployment of increasingly complex distributed embedded systems, engineers are challenged by a plethora of design choices. This often results in infeasible or sub-optimal solutions. In industry and academia, general and domain-specific optimization techniques are developed to explore the tradeoffs within these design spaces, though these techniques are usually not adapted for use within a Model- Driven Engineering (MDE) process. In this paper we propose to encode metaheuristics in transformation models as a general design exploration method. This is complemented by an MDE framework for combining different heterogeneous techniques at different abstraction layers using model transformations. Our approach results in the seamless integration of design space exploration in the MDE process. The proposed methods are applied on the deployment of an automotive embedded system, yielding a set of Pareto-optimal solutions.
Download Technical Report
Maris Jukss and Hans Vangheluwe and Clark Verbrugge, "Implementing Graph Transformation Languages using RDF Storage and SPARQL Queries", School of Computer Science, McGill University, Aug. 15, 2012, CS-TR-2012.3 Abstract
Abstract
The Resource Description Framework (RDF) format has seen significant interest from industry as a flexible format for graph representation. However, RDF has so far not been widely used in the context of graph rewriting tools. In this paper, we take AToMPM, our research-oriented meta-modelling and graph rewriting tool and extend it by adding RDF-based graph transformation functionality. We address the graph matching problem, generating custom SPARQL queries for each rule pattern, and use that to efficiently perform matches on a source RDF graph. In this way we create a research system for RDF graph transformations that also gives us the ability to investigate different possible approaches to using RDF and evaluate the effects on the system. Our experience and performance data serves as a guideline for evaluating the trade-off between the inherent efficiency of a specialized representation and the flexibility of using a standardized representation.
Download Technical Report
Levi Lucio and Joachim Denil and Hans Vangheluwe and Sadaf Mustafiz and Bart Meyers, "The Formalism Transformation Graph as a Guide to Model Driven Engineering", School of Computer Science, McGill University, March 15, 2012, CS-TR-2012.1 Abstract
Abstract
In recent years, many new concepts, methodologies, and tools have emerged, which have made Model Driven Engineering (MDE) more usable, precise and automated. A MDE process is very often dependent on the domain. Thus, means for composing and customizing MDE activities are increasingly necessary. In this paper, we propose the FTG+PM framework that acts as a guide for carrying out model transformations, and as a basis for unifying key MDE practices, namely multi-paradigm modelling, meta-modelling, and model-transformation. The FTG+PM consists of the Formalism Transformation Graph (FTG) and its complement, the Process Model (PM), and charts all kinds of activities in the MDE lifecycle such as requirements development, domain-specific design, verification, simulation, analysis, calibration, deployment, code generation, execution, etc. The FTG describes in an explicit and precise way, formalisms, and their relationships as transformations between formalisms. The PM defines an actual MDE process using these formalisms and transformations. We illustrate the proposed FTG+PM approach through the design of an automated power window, a case study from the automotive domain.
Download Technical Report
Levi Lucio and Joachim Denil and Hans Vangheluwe, "An Overview of Model Transformations for a Simple Automotive Power Window", School of Computer Science, McGill University, Jan. 15, 2012, CS-TR-2012.2 Abstract