Security and Privacy April 2015 Presentations

Security and Privacy Presentations by MSEC research group
Friday 14 April 2015, University of Antwerp

10:40 - 11:15 Vincent Naessens
Research at MSEC

Presentation [ppt]


10:40 - 11:15 Koen Decroix
Inspecting Privacy in Electronic Services

Presentation [pdf]


11:50 - 12:05 Hans Vangheluwe
Modelling, Simulation and Design Lab (MSDL) research "big picture"

Presentation [pdf]


12:05 - 13:15 Lunch


13:15 - 13:30 Bart Meyers
ProMoBox: A Framework for Generating Domain-Specific Property Languages

Specifying and verifying properties of the modelled system has been mostly neglected by domain-specific modelling (DSM) approaches. At best, this is only partially supported by translating models to formal representations on which properties are specified and evaluated based on logic-based formalisms, such as linear temporal logic. This contradicts the DSM philosophy as domain experts are usually not familiar with the logics space. To overcome this shortcoming, we propose to shift property specification and verification tasks up to the domain-specific level. The ProMoBox framework consists of (i) generic languages for modelling properties and representing verification results, (ii) a fully automated method to specialize and integrate these generic languages to a given DSM language, and (iii) a verification backbone based model checking directly plug-able to DSM environments. In its current state, ProMoBox offers the designer modelling support for defining temporal properties, and for visualizing verification results, all based on a given DSM language. We are working on support for test case generation, for the case when model checking is not feasible. We use the example of a simple elevator controller DSL in the presentation, and have applied ProMoBox on other DSLs such as GISMO (for gestural interaction), and a subset of the well-known BPMN (Business Process Model and Notation).

Presentation [pdf][pptx]

References:
Bart Meyers, Romuald Deshayes, Levi Lucio, Eugene Syriani, Manuel Wimmer and Hans Vangheluwe. ProMoBox: A Framework for Generating Domain-Specific Property Languages. In "Proceedings of the 7th International Conference on Software Languages Engineering (SLE 2014)", Lecture Notes on Computer Science, vol. 8706, p. 1-20, 2014.
Romuald Deshayes, Bart Meyers, Tom Mens and Hans Vangheluwe. ProMoBox in Practice : A Case Study on the GISMO Domain-Specific Modelling Language. In "Proceedings of the 8th Workshop on Multi-Paradigm Modeling (MPM 2014)", CEUR Workshop Proceedings, vol. 1237, p. 21-30, 2014.
Bart Meyers, Manuel Wimmer, and Hans Vangheluwe. Towards Domain-specific Property Languages: The ProMoBox Approach. In "Proceedings of the 2013 ACM Workshop on Domain-specific Modeling", p. 39-44, ACM New York, NY, USA, 2013.


13:30 - 13:45 Yentl Van Tendeloo
DEVS simulation & Modelverse

Presentation [pdf]


13:45 - 14:00 Bruno Barroca
Models for Language Engineering

We are currently developing a model of a (meta-)modeling environment. This presents many challenges from the theoretical point of view (e.g., being self-describable, achieving strongly typed relations between models and model elements), but also many practical opportunities (ranging from enhanced performance, and achieving platform-independence with resort to deployment models). With our model we expect to then be able to define a class of modeling environments that can effectively interoperate and integrate seamlessly with existing implementations/realizations.

Presentation [ppt]


14:00 - 14:20 Simon Van Mierlo
Explicit Modelling of Model Debugging Environments

The model-driven engineering approach can only be successful if all phases in the development process are supported by appropriate tools. These tools need to be usable, and in this presentation we focus on one usability aspect: debugging. In software development, debuggers are essential: developers spend a large portion of their time debugging code. We want to bring the same level of control to modelling and simulation environments. To construct a set of useful debugging operators, we take inspiration from both the code debugging world and the simulation world (including different notions of time). We propose to explicitly model the timed, reactive behaviour of the simulator as a Statechart, to minimize accidental complexity. After instrumenting this Statechart with debugging support, we regenerate the code for the (debuggable) simulator. It is then combined with a visual modelling and simulation environment, with which the user can interact with the simulator.

References (Publications):
[1] Simon Van Mierlo, Yentl Van Tendeloo, Sadaf Mustafiz, Bruno Barroca, and Hans Vangheluwe. Explicit modelling of a Parallel DEVS experimentation environment. In Proceedings of the 2015 Symposium on Theory of Modeling and Simulation - DEVS, TMS/DEVS '15, part of the Spring Simulation Multi-Conference, pages 860 - 867. Society for Computer Simulation International, April 2015.
[2] Simon Van Mierlo. Explicit modelling of model debugging and experimentation. In Proceedings of the Doctoral Symposium at MODELS'14, 2014.
[3] Hans Vangheluwe, Daniel Riegelhaupt, Sadaf Mustafiz, Joachim Denil, and Simon Van Mierlo. Explicit modelling of a CBD experimentation environment. In Proceedings of the 2014 Symposium on Theory of Modeling and Simulation - DEVS, TMS/DEVS '14, part of the Spring Simulation Multiconference, pages 379 - 386. Society for Computer Simulation International, 2014.

Presentation [pdf][pptx]


14:20 - 14:40 Cláudio Gomes
Efficient Model Transformations & Co-simulation

After almost a decade of experimental application of model-driven techniques in system's development, it is undeniable the benefits of the usage of modeling and model transformations regarding productivity. However, the level of abstraction employed on the existing model transformation languages do not seem to be adequate to meet industry standards, at least in what matters to run-time performance. We suspect that this may be due to the fact that these languages hide too much detail. Information that could be rather used to speed up transformations, namely pattern matching and its scheduling. In this paper, we search for the most appropriate concepts from both declarative and imperative languages, in order to develop TrNet: a new transformation language whose transformation specifications can be automatically analysed regarding performance, and ultimately optimised. We evaluate our approach by developing a new compiler for the DSLTrans transformation language.

Presentation [pdf]

References:
Classification of Model Transformation Tools: Pattern Matching Techniques
A Framework for Efficient Model Transformations


14:40 - 15:00 Joachim Denil
Design, Verification, Deployment and Evolution of SIS and CPS

Software has become a key component of a rapidly growing range of applications, products and services from all sectors of economic activity. This can be observed in large-scale heterogeneous systems, embedded systems for automotive applications, telecommunications, wireless ad hoc systems, business applications with an emphasis on web services etc. Such systems are commonly called software-intensive systems. Software-intensive systems are characterized by their reactive nature, real-time requirements, mix of continuous and discrete (hybrid) behaviour, the embedded character of some components of the system, the required dependability and the distribution of its elements. Multi-Paradigm Modelling has already been proposed as a method for the development and verification of software-intensive systems. In multi-paradigm modelling every aspect of a system is modelled explicitly, at the most appropriate level(s) of abstraction, using the most appropriate formalism(s). Because multi-paradigm modelling promotes the explicit modelling of all aspects of a system, the process to design, verify and deploy systems has to be explicitly modelled as well. We propose the Formalism Transformation Graph and Process Model (FTG+PM) for this purpose. The FTG+PM contains, on the one hand, the definition of all formalisms and transformations involved in creating software-intensive systems. On the other hand, these formalisms and transformations are used within a process to create the systems. The FTG+PM is applied to the creation of an automotive exemplar, the power window system. Several languages and transformations are identified to create the exemplar. The process starts with the modelling of requirements. Domain-specific languages are used to model different aspects of the system (namely: the environment, plant and control model). These models are transformed to Petri nets for verification and to a hybrid simulation model to evaluate the dynamic behaviour of the system. Finally, the system is deployed to a network of electronic control units. During deployment it is necessary to evaluate the behaviour and other extra-functional properties of the solution. It is however not feasible to build the system and check the behaviour at the implementation level. Therefore, the Discrete Event System Specification is evaluated as an appropriate formalism for the simulation of deployed software-intensive systems. Finally, we evaluate the feasibility of transformations to optimise the deployment of software-intensive systems. A number of methods are used to leverage the explosion of the design-space. Multi-paradigm optimisation uses different optimisation techniques together to solve a single problem. Model transformation allows us to transform models from and to an optimal optimisation representation (for example, MILP). The presented methods, techniques and tools need be available for industrial use, it is therefore necessary to integrate them into current tools. For this purpose we integrate model transformation in the Simulink tool. We show the approach by instrumenting a simulink model with printf blocks for trace purposes while preserving the timing behaviour of our global application.

Presentation [pdf]


15:00 - 15:20 Ken Vanherpen
Model Transformations for Round-Trip Engineering in Control Deployment Co-Design

When developing a control algorithm for a mechatronic system, its deployment on hardware is rarely taken into account. Hardware properties such as execution performance, memory consumption, communication delays, buffer sizes, (un)reliability of the communication channel, etc. are often not the first concern of the control engineer. However, these properties may have important effects on the control loop behaviour such that initial requirements may no longer be fulfilled. To tackle this issue, we propose a Round-Trip Engineering (RTE) method allowing for a semi-automatic integration of hardware properties, corresponding to the deployment, into the control model. The proposed RTE method combines techniques of model transformations and model-based design space exploration. The resulting method will enable an engineer to further enhance the control model based on implementation properties such that the initial requirements are still satisfied when deployed on the target hardware platform.

Presentation [pdf]

References:
Publications


15:20 - 15:35 Bentley Oakes
Model Sanitization

In order to faciliate and encourage collaboration between industrial, research, and tool partners, there is an increased need to share meta-models and models used in modelling-driven development. However, these models may contain the industrial partner's intellectual property (IP), which prevents them being shared freely. In order for the other partners to use these models for experimentation or analysis, it is necessary to remove this IP while retaining the essential properties of the models. In our work, we attempt to develop a tool that can semi-automatically 'sanitize' an Ecore model to remove IP information. This removal process is guided through the use of model queries to dictate which information is removed by the sanitization process, and which information must be retained. Our objective is to provide an Eclipse plugin that is a 'push-button' solution for use by industrial users.

Presentation [pdf]

15:35 - 15:50 Bentley Oakes
Analysis and Optimization of Simulink Models

The Simulink modelling tool is used to diagram and study cyber-physical systems, and to generate embeddable code directly from the models. However, this code generation process means that inefficiencies in the model may be propagated to the code. Optimizations may be performed during code generation, but this may lead to an unacceptable loss of traceability in determining which parts of the model were modified or removed. Our works focuses on defining model-to-model optimizations, where the optimized model can be loaded back into Simulink for further development or analysis. We suggest this improves traceability and can allow model specialization for different platforms. In this work, we present three optimizations to improve model simulation performance and/or the visual layout of the model.

Presentation [pdf]

References:
B. Oakes. Optimizing Simulink Models. (2014) SOCS-TR-2014.5. McGill University.


István Dávid
A Multi-Paradigm Modeling Foundation For Collaborative Multi-view Model/System Development

Semantic inconsistencies are often occurring phenomena in multi-model settings. Addressing this issue requires (i) proper characterization of inconsistencies, and (ii) appropriate techniques for recovery once the inconsistencies are present in the design. As a main contribution, we identify inconsistency tolerance as the key to scalable and efficient inconsistency management and propose formal algebraic foundations to define and evaluate tolerance rules. To support our technique, a tooling for (i) real-time evaluation of tolerance rules and (ii) quick fix generation for semi-automated inconsistency management will be implemented by reusing the techniques of complex event processing (CEP), design space exploration (DSE), model transformations (MT) and reactive programming (RP).

Presentation [SlideShare]

References:
MBSE4Mechatronics


Bert Van Acker
Generic Master Generation

This presentation gives a quick overview on the work that is already done on the FMI standard. It describes the problem, namely the absence of the standardization for the master algorithm. We try to address this by automatically generating Problem-specific master algorithms because these can have a run-time performance benefit against the generic master algorithms. In the current work, we developed a DSL to represent a interaction model of the FMUs and we defined a workflow to obtain a C-code representation of the master algorithm by performing 3 transformations, starting with a set of FMUs/slaves that we want to co-simulate. The future research topic is more focused on the use of Global model management techniques in order to (semi-)automatically generate a proper co-simulation model, based on the desired executed analysis. This includes the selection of the proper model/FMU to populate the co-simulation model in order to optimize the performance of the co-simulation for each type of analysis. There are four major topics : (a) how will we capture and use the analysis characteristics in order to optimize the simulation for it. How will we select the proper models depending on the analysis type? (b)defining the workflow in order to end up with a analysis-optimized co-simulation model. This will need to be as automated as possible. (c) how will we merge the models with the hardware specific aspects(CPU usage, memory) and make this executable. This way we could not only validate the functional behavior but also the non-functional in one simulation when needed for a particular analysis. (d) how will we manage the set of models which will represent one subsystem but with different views and abstractions. There will need to be perfect traceability between model and subsystem but also between the different models of one subsystem. In order to obtain this, we will need to define specific meta-data for each model and capture the global relation between models and subsystems, models and models and of course sybsystems and subsystems to form a system.

Presentation [pdf]

References:
Van Acker, B., Denil, J., Vangheluwe, H., De Meulenaere, P., “Generation of an Optimised Master Algorithm for FMI Co-Simulation”, in Proceedings of the Symposium on Theory of Modeling & Simulation-DEVS Integrative, Society for Computer Simulation International (2015), p946-953