09:00: Coffee at Hans' office (M.G.116)

09:30: welcome and high-level overview (Hans Vangheluwe)

09:40 - 10:00: Keynote: Riding the Line Between the Formal and Non-Formal in Modeling (Rick Salay)

Abstract: Graphical models are a key tool for taming the complexity of developing large systems, yet they lie at the border of some fundamental dichotomies: cognition vs. computation, non-formal vs. formal languages and practice vs. theory. This makes them both interesting and challenging. In my research, I develop formal theories about non-formal concepts like modeler intent and modeler uncertainty in order to provide a foundation for tool support that will help practioners. In this talk I'll briefly illustrate these ideas with examples.

10:00 - 11:10: Session on Modeling Language Engineering

10:00: Modelverse (Yentl Van Tendeloo)

Abstract: The type/instance relation is often identified as the basic building blocks of a metamodelling tool. Despite the credit given to this relation, it is often, partially or completely, hidden in the tool implementation. We identified several problems in the literature, which we believe to be caused by this obfuscation. Our approach explicitly models not only the model and metamodel, but also the type mapping, and even the conformance checking algorithm. Doing so, we obtain an explicit model of what it means to be an instance. This approach allows, for a single model, multiple type models, using multiple typing relations.

10:10: Semantic Languages for Developing Correct Language Translations (Bruno Barroca)

Abstract: The development and validation of language translators (e.g., port programs, language preprocessors, high-level software language compilers, etc.) are time-consuming and error-prone: language engineers need to master both the source and target languages' syntactic constructs; and most importantly their semantics. We will present an approach for developing and validating such language translators based on two languages: With the first, we specify a language translation using a syntax-to-syntax mapping; and with the second, we define the semantics of both of the source and target languages. Finally, we will discuss what could be the next steps on this line of work.

10:20: Modular Language Composition (Cláudio Gomes)

Abstract: The engineering of complex cyber-physical systems (CPS) can greatly benefit from the ability to apply multi-paradigm modeling techniques. These systems can be so heterogeneous that existing modeling languages may not be expressive or appropriate, and new - domain specific ones - may have to be created. A new language will most likely include several aspects – not only syntactic, but also semantic - that are common in some other language. In this work, we tackle the question of how to reuse and combine different fragments of languages in the development of new ones. We apply it in the development of hybrid languages of two well known languages for the modeling and simulation of CPS: Hybrid Automata and Hybrid Causal Block Diagrams.

10:30: Verification of Domain-Specific Models with ProMoBox (Bart Meyers)

Abstract: Verifying whether a model satisfies a set of requirements is considered to be an important challenge in domain-specific modelling (DSM). It is nevertheless mostly neglected by current DSM approaches. We present a solution in the form of ProMoBox, a framework that integrates the definition and verification of temporal properties in discrete-time behavioural domain-specific modelling language (DSMLs), whose semantics can be described as a schedule of graph rewrite rules. Thanks to the expressiveness of graph rewriting, this covers a very large class of problems. With ProMoBox, the domain user models not only the system with a DSML, but also its properties, input model, run-time state and output trace. Additionally generic support is provided to automatically verify these properties, using model checking techniques. Moreover, the ProMoBox techniques can be adapted to be used in testing, and in test case generation.

10:40: Dynamic Structure Modelling for Causal Block Diagrams (Yves Maris)

Abstract: Dynamic structure systems can undergo changes to its network structure at any point in time during simulation. This can include the addition, removal or modification of components or relations between component. Allowing this type of behaviour can greatly improve expressiveness of a modeling language. We extended causal block diagrams with dynamic structures in a way that is consistent with its standard constructs. Model transformation is allowed trough the addition of a new concept, structure blocks, to the existing language. New components are instantiated and existing ones are removed as specified within the structure block. As a proof of concept we implemented an exhaustive model in a prototype simulator for the new extended language. This work is also a step forward in finding the essence of dynamic structure modeling.

10:50: 20 min discussion

11:10: coffee

11:20 - 12:30: Session on Simulation Techniques

11:20: PythonPDEVS (Yentl Van Tendeloo)

Abstract: PythonPDEVS is a Python-based DEVS simulation kernel for both Classic and Parallel DEVS. Existing DEVS simulation kernels have primarily focussed on either features or performance, mostly neglecting the other. With PythonPDEVS, we provide a rich set of features, such as support for multiple DEVS formalisms, realtime simulation, and distributed simulation. Performance being another of our design goals, we implemented various performance optimizations. PythonPDEVS is briefly compared to similar in terms of feature set and performance.

11:30: SCCD: a Statecharts and Class Diagrams hybrid (Simon Van Mierlo)

Abstract: We introduce the SCCD formalism: a Statecharts and Class Diagrams hybrid. SCCD facilitates the specification of complex timed, reactive, interactive discrete event systems (e.g., complex user interfaces), as we demonstrate using a representative example. We present a SCCD compiler that supports (a) semantic variation points for different Statecharts variants (e.g., Rhapsody, Statemate, etc.), (b) code generation for different platforms (e.g., Tkinter, browser, etc.), and (c) code generation for different families of runtimes (e.g., event-based platforms, game loops, etc.). Furthermore, we discuss the history and future work of SCCD to reveal our research agenda.

11:40: Discontinuity Propagation in Hybrid System Simulation (Cláudio Gomes)

Abstract: Physical systems are inherently continuous. As such, creating detailed models of these is difficult, if not unfeasible. Fortunately, hybrid models that abstract away fast behaviors can greatly simplify the study of such systems. For example, impulses are often used as an intuitive abstraction of a very stiff change in the state of the system that occurs, for instance, in collisions. Given the mathematical peculiarities of impulses, it becomes difficult to define properly what kind of numerical operations can be performed on impulses, for the purpose of simulation of differential equations. In this work, we extend the Causal Block Diagrams (CBD) formalism with impulses and we give a theoretical foundation for each operation in terms of distribution theory. This enables the invariants such as the fundamental theorem of calculus to be kept even in the presence of impulses and discontinuities. The result is a formalism that can accurately simulation a class of hybrid systems. We show a simple example of a bouncing ball and study the performance and accuracy of the simulator when impulses are used.

11:50: Co-simulation: Simulator Coupling Approaches (Cláudio Gomes)

Abstract: Late integration is identified as a major source of problems in modern concurrently developed systems. Modeling and simulation techniques are used to detect wrong assumptions earlier and cheaply in the development process. As systems become more complex, different modeling languages and tools are used to develop different components. To be able to study the interactions between models of different components, one of the possibilities is to make the simulators of each model communicate. Co-simulation is a technique to couple simulators, each responsible for a single model, often seen as a black box, in order to perform simulation of the whole system. In this work we survey the existing approaches to co-simulation. When two simulators are coupled, their models are also coupled, making it of extreme importance that this coupling, sometimes standing for the physical coupling of components, s physically meaningful. We survey the techniques used to ensure the physical correctness and we propose a way in which these can be complemented with techniques to ensure other correctness properties of the coupling.

12:00: Debugging (Simon Van Mierlo)

Abstract: Support for interactive simulation model debugging is currently limited. This is mainly due to its inherent complexity: the interplay of formalism execution semantics, different notions of simulated time such as (scaled) real-time and as-fast-as-possible execution, as well as user interaction through a visual interface are all challenging to capture and correctly implement using traditional software development techniques. We construct visual modelling, simulation, and debugging environments for different simulation formalisms, by explicitly modelling them using Statecharts.

12:10: 20 min discussion

12:30: lunch (sandwiches)

13:30 - 14:40: session on processes and optimization

13:30: FTG+PM (Hans Vangheluwe)

Abstract: To enable Multi-Paradigm (multi-formalism and multi-abstraction) modelling, it is necessary to explicitly model all aspects of the Model-Based Systems Engineering (MBSE) enterprise. A crucial part of this is the explicit modelling of MBSE processes in the form of a Process Model (PM). To explicitly chart the different formalisms used as well as their relationships, the Formalism Transformation Graph (FTG) is introduced. The combination of both, the FTG+PM allows a clear high-level description of MBSE projects.

13:40: Engineering Process Transformation to Manage (In)Consistency (István Dávid)

Abstract: Inconsistencies pose a severe issue to overcome in collaborative modeling scenarios, especially in settings with different domains involved. This is due to the significantly different formalisms employed that have overlapping semantic domains. A pertinent example are today’s mechatronic and Cyber-Physical Systems. We propose an approach for managing inconsistencies based on explicitly modeled linguistic and ontological properties. We argue that to fully understand the reasons of their occurrence and impact on the overall design, inconsistencies should be investigated in the context of the process they emerge in. For this purpose, we propose a language for modeling processes in conjunction with the properties of the engineered system. Characteristics of inconsistencies are identified in terms of process models and properties, and a method for optimal selection of management techniques via multi-objective design-space exploration is provided.

13:50: Tool and Contracts for the Co-Design of Cyber-Physical Systems (Ken Vanherpen)

Abstract: Cyber-Physical Systems are becoming more and more complex and often requires a close cooperation among the various design teams to meet the strict project goals. In current design processes, however, each design team is concerned with implementing a specific (set of) requirement(s) of the system under design with incomplete knowledge of overlapping concerns among design teams. This leads to time consuming, iterative design processes where inconsistencies are resolved, in turn possibly creating new ones. By formalising the interrelationships between the different design teams, we allow engineers to reason about depending cross-domain properties and hence to manage inconsistencies. Therefore, we introduce ontological properties and their relations as a means to reason about the relationships between different design teams. In our research, we limit our focus on control-deployment co-design.

14:00: Experimental Frames (Joachim Denil)

Abstract: Because of the act of modelling, a model of a real-world system is only valid in a certain context. Zeigler defines the "experimental frame" as the set of experiments for which the model is valid. However, because the experimental frame concept is underspecified and because the use is depending on the engineering goal, it is very difficult to implement such an experimental frame. In this work we distinguish between the three different engineering goals of an experimental frame: (a) the experiment model, as the process model of an experiment to reproduce the results, (b) the validity frame, as the frame to look at validity of a model in a certain context or calibration of a model, and (c) the property frame, to look at the properties and substitutability of a model.

14:10: Agility in the MBSE Process (Joachim Denil)

Abstract: The Agile Manifesto promotes a set of principles and guidelines for software development to better cope with changing requirements. The promise of coping with changing requirements is also appealing to the systems engineering community. However, new methods, techniques and tools should be created to allow for agility in the MBSE process.

14:20: 20 min discussion

14:40: coffee

15:00 - 15:30: session on deployment/resource optimized execution

15:00: Deployment for AUTOSAR (Joachim Denil)

Abstract: AUTOSAR (AUTomotive Open System ARchitecture) is an open and standardised automotive software architecture, developed by automobile manufacturers, suppliers and tool developers. Its design is a direct consequence of the increasingly important role software plays in vehicles. As design choices during the software deployment phase have a large impact on the behaviour of the system, designers need a method to explore various trade-offs. In this presentation, we look at some of the work done in modelling and simulating AUTOSAR-based systems.

15:10: Activity in PythonPDEVS (Yentl Van Tendeloo)

Abstract: While DEVS is a very general formalism, even often termed as "the simulation assembly language", simulation performance can be disappointing. This is primarily caused due to the lack of information on the model and the problem domain. Through the use of activity hints, or so called "leaky abstraction", we provide a way for modellers to augment their DEVS model with additional domain information. This information is optionally used by the simulation kernel to achieve significant speedup results. Support for activity in PythonPDEVS is briefly highlighted through its support for polymorphic data structures and intelligent load balancing.

15:20: 10 min discussion

15:30 - 16:00: session on model transformation

15:30: Efficient and Usable Model Transformations (Maris Jukss - Skype)

Abstract: Efficiency, scalability, and usability are of significant concern in the application of model transformation systems to industrial problems. Scalability concerns in terms of graph matching magnify greatly with the input graph size, and best performance is achieved through the use of highly optimized, system-specific designs for graph storage and management. On the other hand pattern matching is the most expensive part of rule based model transformation system, thus efficiency is highly dependent on the capability of the subgraph matching algorithms, where the underlying subgraph isomorphism problem is known to be NP complete. We address efficiency by emphasizing the use of scopes in model transformations. Model transformation usability can be further enhanced with the comprehensive debugging facilities. Not only we are interested in what the transformation does but how the transformation does it.

15:40: Fully Verifying Graphical Contracts on Model Transformations (Bentley Oakes - Skype)

Abstract: As model transformations are a required part of model-driven development, it is crucial to provide techniques that address their formal verification. Our approach is based upon that of symbolic execution, as symbolic abstraction in these techniques allows graphical contracts to be exhaustively proved for all executions of a given program. Our algorithm builds a finite set of path conditions which represents all concrete transformation executions. We are then able to prove contracts over all transformation executions in a model-independent way. This is done by examining if any created path condition violates a given contract, which will produce a counterexample if the property does not hold for the transformation. We present a number of applications of our work, such as the verification of an industrial case study. As well, we showcase SyVOLT, a plugin for the Eclipse development environment for the verification of structural pre- /post-condition contracts on model transformations. The plugin allows the user to build transformations in our transformation language DSLTrans using a visual editor. Finally, we discuss our current approach to the verification of ATL transformations, which is performed by employing a higher-order transformation.

15:50: 10 min discussion

16:00: social event: beer tasting