Keynotes
This year, STAF is proud to feature the following outstanding keynote speakers:
- Juan de Lara: Approaches to model transformation reuse: From concepts to a-posteriori typing
- Juergen Dingel: Complexity is the Only Constant: Thoughts on Trends in Computing and Their Relevance to MDE
- Kim G. Larsen: From Testing and Verification to Performance Analysis and Synthesis of Cyber-Physical Systems
- Gul Agha: Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems
- Erika Ábrahám: Satisfiability Checking: Theory and Applications
- Krzysztof Czarnecki: A Model-Based Driver’s License for Self-Driving Cars: Challenges and Future Directions
- Klaus Reichl: Using Formal Methods for Verification and Validation in Railway
- Stefan Voget: Usage of domain specific modeling languages in the automotive industry
Approaches to model transformation reuse: From concepts to a-posteriori typing
Juan de Lara, Universidad Autónoma in Madrid, Spain
ICMT Keynote on Monday, July 4, 09:00 – 10:30, room EI 9
Models are the main assets of Model-Driven Engineering (MDE), and hence model transformations are essential to automate the model manipulations required by MDE. Different kinds of transformations are common in MDE, like in-place, model-to-model, or model-to-text. In all cases, their definition is based on the meta-models of the models to be manipulated. However, the proliferation of meta-models in MDE (e.g., in connection with Domain-Specific Languages, DSLs) complicates transformation reuse. This is so as transformations are defined for particular meta-models and are not applicable to other meta-models, even if they have some commonalities. Therefore, in order to facilitate the creation of DSL-based MDE solutions, flexible means to reuse transformations across heterogeneous meta-models are required.
In this presentation, we will explore several approaches to transformation reuse. First, taking inspiration from generic programming, we propose concepts, gathering the requirements needed from meta-models to qualify for a model transformation [1]. This way, transformations are defined over concepts and become reusable by binding the concept to concrete meta-models. The binding induces an adaptation of the transformation, which becomes applicable to the bound meta-model. Concepts can also be interpreted as meta-meta-models defining a set of candidate meta-models for the transformation. Hence, we will explore multi-level modelling to express reusable transformations [3]. However, this approach requires using the domain meta-meta-model to construct the meta-models and prevents unanticipated reuse. Hence, the talk will end presenting a-posteriori typing. This is as a means to provide models with additional types beyond their creation meta-model [2], so that transformations defined for such types become reusable for those models. Moreover, decoupling object creation from typing permits embedding simple transformations in the conformance relation.
References:
- J. de Lara and E. Guerra. From types to type requirements: genericity for model-driven engineering. Soft. and Syst. Modeling, 12(3):453–474, 2013.
- J. de Lara, E. Guerra, and J. S. Cuadrado. A-posteriori typing for model-driven engineering. In MoDELS, pages 156–165. IEEE, 2015.
- J. de Lara, E. Guerra, and J. S. Cuadrado. Model-driven engineering with domain-specific meta-modelling languages. Soft. and Syst. Modeling, 14(1):429–459, 2015.
Biography:
Juan de Lara is associate professor at the computer science department of the Universidad Autónoma in Madrid, where he coordinates the modelling and software engineering research group (miso). He holds a PhD in computer science since 2000, and his current research interests lie in Model-Driven Engineering, in aspects like meta-modelling, multi-level modelling (realized in the MetaDepth tool), domain-specific languages and the analysis of model transformations. He has spent research periods at McGill University (where he developed the AToM3 tool within the MSDL lab), TU Berlin, Sapienza University of Rome and the University of York. He has been PC co-chair for ICMT’12 and FASE’12 and he is in the editorial board of the SoSyM journal.
Complexity is the Only Constant: Thoughts on Trends in Computing and Their Relevance to MDE
Juergen Dingel, Queen’s University, Ontario, Canada
ICGT Keynote on Tuesday, July 5, 09:00 – 10:30, room EI 7
The talk will discuss the central role that the fight against complexity has played in the relatively short but eventful history of computing and is likely to continue to play. The importance of key MDE concepts — abstraction, automation, and analysis — in this fight will be highlighted. Also, some research efforts and technology trends in computing and society will be discussed and their potential relevance to modeling will be argued. For instance, work in the programming languages community on synthesis and trends in science and society towards increased “openness” and transparency will be of particular interest. Potential research opportunities for different research communities, such as graph transformation and formal methods, will be highlighted.
Biography:
Juergen Dingel is Associate Professor in the School of Computing at Queen’s University in Kingston, Canada. He received an M.Sc. in Computer Science from Berlin University of Technology in 1992, an M.Sc. in Pure and Applied Logic in 1994 and a Ph.D. in Computer Science in 1999 from Carnegie Mellon University. He is vice chair of the MODELS Steering Committee, and a member of the editorial board of the Springer journal Software and Systems Modeling (SoSyM). He was PC Co-chair of the ACM/IEEE 17th International Conference on Model Driven Engineering Languages and Systems (MODELS’14) in Valencia and of the IFIP International Conference on Formal Techniques for Distributed Systems (FMOODS-FORTE’11) in Reykjavik. At Queen’s, he leads the Modeling and Analysis in Software Engineering Group (MASE). His research interests revolve around the definition and use of rigorous notations and techniques for the development and analysis of software artifacts and he has published extensively on these topics. He has collaborated with a range of industrial partners including IBM, GM, and Ericsson.
From Testing and Verification to Performance Analysis and Synthesis of Cyber-Physical Systems
Kim G. Larsen, Aalborg University, Denmark
TAP Keynote on Tuesday, July 5, 14:00 – 15:30, room EI 7
Timed automata and games, priced timed automata and energy automata have emerged as useful formalisms for modeling real-time and energy-aware systems as found in several embedded and cyber-physical systems. In this talk we will survey how the various component of the UPPAAL tool-suite over a 20 year period has been developed to support various type of analysis of these formalisms. This includes the classical usage of UPPAAL as an efficient model checker of hard real time constraints of timed automata models, but also the branch UPPAAL TRON which have been extensively used to perform on- and off-line conformance testing of real-time systems with respect to timed automata specifications. More ambitiously, UPPAAL TIGA allows for automatic synthesis of strategies – and subsequent executable control programs – for safety and reachability objectives. Most recently the branch UPPAAL SMC offers a highly scalable statistical model checking engine supporting performance analysis of stochastic hybrid automata, and the branch UPPAAL STRATEGO supports synthesis (using machine learning) and evaluation of near-optimal strategies for stochastic priced timed games. The keynote will review the various branches of UPPAAL and indicate their concerted applications to a range of real-time and cyber-physical examples.
Biography:
Kim G. Larsen is a professor in the Department of Computer Science at Aalborg University within the Distributed and Embedded Systems Unit and director of the ICT-competence center CISS, Center for Embedded Software Systems. In 2015, he won an ERC Advanced Grant with the project LASSO for learning, analysis, synthesis and optimization of cyber physical systems. He is also director of the Sino-Danish Basic Research Center IDEA4CPS, the Danish Innovation Network InfinIT, as well as the newly founded innovation research center DiCyPS: Data Intensive Cyber Physical Systems. Kim G Larsen is prime investigator of the tool UPPAAL and co-founder of the company UP4ALL International. In 2013 he was the recipient of the CAV Award for his work on UPPAAL as “the foremost model checker for real-time Systems”. Kim G Larsen became Honorary Doctor (Honoris causa) at Uppsala University, Sweden, in 1999. In 2007 he became Knight of the Order of the Dannebrog. In 2007 he became Honorary Doctor (Honoris causa) at ENS Cachan, France. In 2012 he became Honary Member of Academia Europaea. Since 2016 he has been appointed INRIA International Chair for a 5 year period.
Abstractions, Semantic Models and Analysis Tools for Concurrent Systems: Progress and Open Problems
Gul Agha, University of Illinois at Urbana-Champaign, USA
SEFM Keynote 1 on Wednesday, July 6, 09:00 – 10:30, room EI 7
The growth of mobile and cloud computing, cyberphysical systems and the internet of things has arguably made scalable concurrency the dominant form of computing. I will describe the state of the art in models of concurrency, programming abstractions and analysis tools. I will then summarize how actor languages and frameworks have been widely adopted to address scalability, and how new tools that combine static and dynamic analysis are making software safer. However, as we scale up cyberphysical applications and build the internet of things, a key limitation of current languages and tools becomes apparent: the difficulty of representing quantitative and probabilistic properties and reasoning about them. While considerable research has been done in this area, many open problems remain. I will conclude by prioritizing problems that need to be addressed before we can build more complex scalable concurrent applications.
Biography:
Gul Agha is Professor of Computer Science at the University of Illinois at Urbana-Champaign. Agha is a Fellow of the IEEE and a recipient of the IEEE Computer Society Meritorious Service Award. He served as Editor-in-Chief of IEEE Concurrency: Parallel, Distributed and Mobile Computing (1994-98), and of ACM Computing Surveys (2000-2007). While Agha is best known for his work on the formalization of the Actor Model and the development of actor languages, he has also led his research group in pioneering research on statistical model checking, concolic testing, computational learning for verification, and in developing a computational model for energy complexity of parallel algorithms. Agha is the co-director of the interdisciplinary Illinois Structural Health Monitoring Project which has developed sensor networks to monitor civil infrastructure, and a co-founder of Embedor Technologies which is using actor inspired distributed computing to enable continuous monitoring of bridges for improved maintenance and anomaly detection.
Satisfiability Checking: Theory and Applications
Erika Ábrahám, RWTH Aachen University, Germany
SEFM Keynote 2 on Wednesday, July 6, 14:00 – 15:30, room EI 7
Satisfiability checking aims to develop algorithms and tools for checking the satisfiability of existentially quantified logical formulas. For propositional logic, in the late ’90s impressive progress was made towards practically applicable solutions, resulting in powerful SAT solvers. Driven by this success, a new line of research started to enrich propositional SAT solving with solver modules for different theories. Nowadays, sophisticated SAT-modulo-theories (SMT) solvers are available for, e.g., equality logic with uninterpreted functions, bit-vector arithmetic, array theory, floating point arithmetic, and real and integer arithmetic. SAT and SMT solvers are now at the heart of many techniques for the analysis of programs and probabilistic, timed, hybrid and cyber-physical systems, for test-case generation, for solving large combinatorial problems and complex scheduling tasks, for product design optimisation, planning and controller synthesis, just to mention a few well-known areas.
In this talk we give an introduction to the theoretical foundations of satisfiability checking and discuss the efficient embedding of SAT and SMT solvers in different software technologies.
Biography:
Erika Ábrahám graduated at the Christian-Albrechts-University Kiel (Germany), and received her PhD from the University of Leiden (The Netherlands) for her work on the development and application of deductive proof systems for concurrent programs. Then she moved to the Albert-Ludwigs-University Freiburg (Germany), where she started to work on the development and application of SAT and SMT solvers. Currently she is professor at RWTH Aachen University (Germany), with main research focus on SMT solving for real and integer arithmetic, and formal methods for probabilistic and hybrid systems.
A Model-Based Driver’s License for Self-Driving Cars: Challenges and Future Directions
Krzysztof Czarnecki, University of Waterloo, Canada
ECMFA Keynote on Thursday, July 7, 09:00 – 10:30, room EI 7
Vehicles with limited self-driving capabilities are already on the market and some car makers have promised products capable of autonomous driving in an urban setting in 2020. Self-driving cars will eventually completely transform the automotive industry, replacing private car ownership by service-based products such as robotic cabs. The deployment of large-scale self-driving vehicle fleets will reduce the number of crashes and crash severity, reduce emissions, allow commuters to use their time more effectively, and free up spaces occupied by parked cars. The engineering of self-driving cars requires sophisticated models of the environment and the electronic driver system in order to develop the necessary perception and motion planning and control functions. While current self-driving technologies have improved immensely in recent years, a major challenge is assuring the safe operation of an autonomous vehicle in all traffic situations and all road conditions. I will present a reference architecture for self-driving cars and use it to describe the types of models used in engineering of such systems. I will then focus on the challenges of assuring model-based engineering of self-driving cars. I will close by outlining promising directions to address these challenges.
Biography:
Krzysztof Czarnecki is a Professor of Electrical and Computer Engineering at the University of Waterloo. Before coming to Waterloo, he was a researcher at DaimlerChrysler Research (1995-2002), Germany, focusing on improving software development practices and technologies in enterprise, automotive, and aerospace domains. He co-authored the book on
Using Formal Methods for Verification and Validation in Railway
TAP Industrial Keynote on Thursday, July 7, 14:00 – 15:30, room EI 7
A very promising and efficient method of showing the correctness of a complex system is using formal methods on a model of that system. To this end there exist plentiful methods and tools for easing the mathematically burdensome process of refinement and proofs as well as the computationally complex task of model checking. While in todays industrial applications formal methods are mostly used for verification (i.e. for showing that the system model fulfills properties such as completeness and consistency) we propose to use these methods for validation as well (i.e. correspondence of the model with the customer needs).
In this paper we show the applicability as well as the limitations of this approach for feature driven development towards continuous verification and validation. As an example we present a model of a railway interlocking system written in Event-B. The model can be instantiated and animated which, in combination with model checking and formal proofs, demonstrates the usefulness of the approach. The resulting model can be used again to automatically generate test cases which are suitable to show the correspondence of the implementation and the model, given that the model supports a sufficient level of detail.
Biography:
Klaus Reichl is a Senior System and Software Architect at Thales Ground Transport Division in charge of engineering highest quality solutions in the safety critical area of railway applications. He received his master degree from Vienna University of Technology in 1986. After the development of fault tolerant, real-time computation and communication platforms in the late 1990s, he has been entering the core business development of train signalling and is currently engaged in architecting and modeling signalling applications. In his spare time, he loves playing guitar, indoor and outdoor, and is hiking and skiing the mountains, mostly outdoor. Klaus can be found on LinkedIn and Google+.
Usage of domain specific modeling languages in the automotive industry
Stefan Voget, Continental Automotive GmbH, Germany
ECMFA Industrial Keynote on Thursday, July 7, 16:00 – 17:00, room EI 9
Before the introduction of model based engineering, the answer for the language question within the automotive industry was simple: use C. The idea of model based engineering is to shift the complexity out of a textual representation of the code (the source code in C) to a model. Here, the question about language comes up again. This time, it revolves around the decision which language to use to represent the model. Today, the answer is not that simple anymore. Within the automotive industry nearly each project uses its own representation. Often the representation is determined by the architectural tool used in the project. To become independent from these “tool languages”, more and more domain specific modeling languages come up, most of which end up as project specific modeling languages, i.e. specific languages used only in a very dedicated context. In the keynote I will present a motivation for the definition and usage of domain specific modeling languages by using two examples. The first example integrates the development lifecycle of a SW developer with the one of a responsible for functional safety. The second example describes a unified approach for the configuration of different software platforms. Both examples and their motivations are quite different from each other, but show the needs for comprehensive common languages and the importance of model to model transformations to interact between them.
Biography:
Stefan Voget is head of HW/SW Innovations in the central strategy and technology department of Continental Automotive in Regensburg, Germany. Mr. Voget got his doctoral thesis in informatics and mathematics in 1996. From 1997 to 2005 he worked on SW-architecture projects for Robert Bosch GmbH. He changed 2005 to Siemens VDO Automotive in Regensburg. He represented the company as project leader in the AUTOSAR consortium worked for several years as product manager for AUTOSAR products. In 2011 he changed to the innovation department in Continental Automotive and led an international funded project “SAFE” about process interpretation of ISO26262. Since 2014 he works for innovation topics for the automated driving area.
