Fall Days on Models for Constructing Software
Center Parcs Zandvoort, Zandvoort (see e.g. Google maps)
November 4-8, 2024
The IPA Fall Days are an annual multi-day event, dedicated to a specific theme of current interest to the research community of IPA. This year’s Fall Days are titled
Models for Constructing Software
Software engineering in the high-tech industry increasingly requires an interdisciplinary approach and teamwork between experts from various domains. Combined with the traditional challenges of software engineering and the quality standards set by these industries, delivering high-quality software is immensely challenging. To bridge the gap between domains, formal models and domain-specific languages can be a great tool. Extending these with a digital twin helps to gain further insights. Moreover, models are a great asset when applying formal verification techniques. In the IPA Fall Days 2024, we will discuss all these techniques and how they relate and reinforce each other.
Programme
The programme is composed by Tanja Vos (OU), Vadim Zaytsev (UT) and Victoria Degeler (UvA), assisted by Thomas Neele (IPA).
On Tuesday 5 November, we will have a special morning session around the IPA Dissertation Award for the best IPA dissertation from 2023
Social Events
On Monday, there will be drinks on IPA after the dinner. On Wednesday afternoon and evening, an edition of the by now famous IPA social events will once again be organised by the IPA PhD council.
Schedule
The schedule below will be updated regularly with the latest information on the program.
Monday November 4th
| 11:15–12:15 | Registration |
| 12:30–13:30 | Lunch at Rise & Shine Restaurant |
| 13:30–13:40 | Opening |
| 13:40–14:40 | Pieter Pauwels (TU/e) Digital Twinning in the Building and Construction Sector: Models meeting the Domain
Models are of utmost importance in the Architecture, Engineering, and Construction (AEC) sector. Every building or piece of infrastructure (bridge, tunnel, road) is nowadays always constructed digitally first, resulting in a digital shadow of the building (3D object-oriented model), and ideally a digital twin eventually. Such a twin is at best achieved during the operational phase of the building, when smart systems are installed in the building that enable a bidirectional communication with a digital model (control, lighting systems, HVAC systems). Several practical real-world examples will be presented during this talk. The most ubiquitous challenge by far in this industry, however, is the myriad of competing models present for any built artefact, in all phases of the building leading to an unsolvable interoperability challenge (Babylon). This presentation gives an insight in this situation, including a review of building modelling software (BIM software) and Building Management Systems (BMS) and their challenges. The use of a standardized interoperable language is explained, including its failures. Furthermore, the use of formal ontology languages is presented, including a patchwork of formal vocabularies and corresponding datasets. A transition to the web is currently taking place; and this transition will be presented, as it seems to provide a way out of the interoperability challenge by keeping multiple models separated (decentralized and modular model and software development) and requiring appropriate multi-modelling instead of a single source of truth model. |
| 14:40–15:25 | Tom Mens (University of Mons) Model Testing of Executable Statecharts - Why we Need it and How to Do it
Statecharts constitute an executable modelling language for event-based reactive systems. The complexity of statechart models induces the need for model testing and validation techniques, inspired by existing techniques coming from the domain of agile test-driven software development. We propose an approach for testing and validation techniques such as unit testing, behaviour-driven modelling, design by contract, and runtime properties. The approach is supported by Sismic, an open-source statechart interpreter library in Python.Useful pointers:
|
| 15:25–16:00 | Coffee break |
| 16:00–16:45 | PhD intro talks (4x) |
| 16:45–17:30 | Check in for accommodation |
| 18:00–20:00 | Dinner at The Market Restaurant |
| 20:00–21:30 | Welcome drinks at Flip Flop Café |
Tuesday November 5th
| 09:00-09:45 | Yanja Dajsuren (TU/e) Navigating the PhD Journey and Beyond: Driving Innovation Through Software Engineering
Software drives innovation across industries, offering PhD researchers in computer science unique opportunities to explore interdisciplinary applications and make impactful contributions. This talk is organized into three parts. Part 1 focuses on the PhD journey, where managing complex projects requires strong project and stakeholder management, along with technical expertise. I’ll share the top 5 strategies for leading successful projects, drawing from both personal and shared experiences including Sangeeth’s journey. Part 2 shifts to the post-PhD phase, particularly for those planning to pursue an academic career. I’ll discuss the top 5 tips for developing successful research proposals, especially for national and EU grants, and provide insights on conducting impactful, cross-domain research. Part 3 highlights research outcomes in automotive, Cooperative Intelligent Transport Systems (C-ITS), and agriculture, illustrating how software innovations drive progress in these key areas.Bio: Dr. Yanja Dajsuren is the program director of the EngD Software Technology program and assistant professor at the Department of Mathematics and Computer Science, Eindhoven University of Technology (TU/e). She holds a PhD in Computer Science and a Doctorate in Engineering (EngD) degree in Software Technology from the TU/e. Prior to her PhD research in the area of automotive software architecture and engineering field, she worked as a scientist and senior scientist for half a decade working on various advanced software development projects at the Philips Research Lab, NXP Semiconductors (former Philips Semiconductors), and Virage Logic. |
| 09:45-10:30 | Loek Cleophas (TU/e) Painting a landscape — Driving Sangeeth’s Road of Ambition
In this talk, I will discuss how Sangeeth’s character and PhD project lead to his dissertation and winning of the IPA Dissertation Award 2023. I will also briefly contextualize the research in the dissertation—the bigger picture, and (possible) next steps for this research area (as well as Sangeeth). |
| 10:30–11:00 | Coffee break |
| 11:00–11:15 | Handing over IPA Dissertation Award 2023 |
| 11:15–12:15 | Sangeeth Kochanthara (Astron & TU/e) From Setbacks to Success: The Anatomy of a PhD Journey
PhD journeys are rarely straightforward. In this talk, I will share the twists and turns of my PhD experience—the setbacks that ultimately shaped my dissertation and continue to shape my journey post-PhD. |
| 12:30–13:30 | Lunch at Rise & Shine Restaurant |
| 13:30-14:30 | Tijs van der Storm (CWI & RUG) Testing DSLs with DSLs with Rascal and TESTAR
Domain-specific languages are software too, so we need to test them! In this talk I will introduce and demonstrate how custom DSLs for testing DSLs. When testing a DSL, it is essential to focus on both the language’s implementation (including syntax, type checking, evaluation and rendering) as well as the correct execution of the code generated by the compiler. These aspects ensure the DSL is both robust and effective in its intended domain. In this talk I will approach this from two angles, in the context of QL, a DSL for questionnaires. For testing the language implementation part, we will use a DSL, named TestQL, which been explicitly written in Rascal for testing purposes. For the execution part, we will employ automated scriptless GUI testing with TESTAR to verify the execution of the generated code. But that is not all—the oracles used during the scriptless testing will be automatically generated by using the domain-specific knowledge of state invariants within the DSL, demonstrating how domain knowledge can enhance testing effectiveness. |
| 14:30-15:00 | PhD intro talks (3x) |
| 15:00–15:30 | Coffee break |
| 15:30–16:15 | Ulyana Tikhonova (F1RE) The fellowship of DSLs: language workbenches and the LionWeb initiative
Language workbenches are tools that provide high-level mechanisms for the implementation of domain-specific languages (DSLs). They support creation of all essential components of a DSL, such as its metamodel or abstract structure, editing environments or notations, interpretation or code generation, scoping, type system, etc. While there exist many language workbenches that provide powerful tool sets for language engineers, their major drawback is the strong tool lock-in: any solution that you implement in one language workbench is impossible to export into another one. The LionWeb initiative was started to overcome this disadvantage. The LionWeb protocol aims at facilitating the interoperability between various language engineering tools and, in this way, allowing for the reuse of language engineering components and modeling tools. In my talk I will demonstrate one of the most used modern language workbenches, JetBrains MPS, and will show how I can connect it via the LionWeb protocol with another language workbench, Rascal. |
| 16:15–17:00 | Ivan Kurtev (Capgemini & TU/e) Model-based Component Engineering with ComMA |
| 17:10–19:10 | Dinner at Rise and Shine |
Wednesday November 6th
| 09:00–09:45 | Petra van den Bos (UT) Coverage-Based Testing with Symbolic Transition Systems
We provide a model-based testing approach for systems comprising both state-transition based control flow, and data elements such as variables and data-dependent transitions. We propose test generation and execution, based on model-coverage: we generate test cases that aim to reach all transitions of the model. To obtain a test case reaching a certain transition, we need to combine reachability in the control flow, and satisfiability of the data elements of the model. Concrete values for data parameters are generated on-the-fly, i.e., during test execution,such that received outputs from the system can be taken into account for the inputs later provided in test execution. We applied our method on the Bounded Retransmission Protocol benchmark. |
| 09:45–10:15 | Coffee break |
| 10:15–11:15 | Theo Ruys (Axini) The practice of Model-Based Testing |
| 11:30–12:15 | PhD intro talks (4x) |
| 12:30–13:30 | Lunch |
| 13:30–14:15 | Burcu Kulahcioglu Ozkan (TUD) Model-guided Testing of Distributed Systems
Coverage-guided randomized testing is effective in finding corner-case bugs in software. However, existing coverage metrics, such as code coverage, are designed for sequential programs, and they are not suitable for assessing the coverage of distributed system behaviors.We present a coverage notion and coverage-guided testing algorithm for distributed systems implementations. Our main innovation is the use of an abstract formal model of the system that is used to define coverage. Our evaluation shows that guiding random test generation using model coverage effectively covers interesting points in the implementation state space.Bio: Burcu Kulahcioglu Ozkan is an assistant professor and Delft Technology Fellow in the TU Delft Software Engineering Research Group. She received her PhD from Koç University Istanbul, Turkey, followed by postdoctoral research at the Max Planck Institute for Software Systems (MPI-SWS) in Kaiserslautern, Germany. Her research focuses on model checking, software testing, and debugging of concurrent programs and distributed systems. |
| 14:15–15:00 | Tom van Dijk (UT) Synthesis of reactive systems In this talk, we explore an overview of reactive synthesis. Contrary to verification or model checking, where an existing system is checked against some formal specification, reactive synthesis is about automatically constructing a system that is guaranteed to satisfy a given specification.
We consider reactive synthesis via automata and games, also known as Church synthesis, which involves constructing a system based on a formal specification, ensuring correctness by design. We start with a formal specification in linear temporal logic (LTL), which we can translate to an automaton that accepts the same language as the specification. The most convenient automaton type for synthesis has a parity winning condition. From this automaton, we construct a game. The solution of the game can be understood as a Mealy machine or an input-output transducer that represents the controller for the system.
The automaton represents the possible behaviors of the system, and the game represents the interaction between the system and its environment. The environment provides inputs, and the system must respond in a way that satisfies the given specification. By solving the game, we derive a strategy that guarantees the system will meet the requirements, regardless of how the environment behaves.
The resulting Mealy machine can be translated into hardware or software, providing a concrete implementation of the controller. This implementation can be used in applications such as robotics, circuit design, or any reactive system where continuous interaction with the environment is required. The advantage of this approach is that it provides correctness by construction, ensuring that the synthesized system always adheres to the given specification.
|
| 15:00-18:00 | IPA PhD Council Social Event |
| 18:00-20:00 | Dinner at Rise and Shine |
| 20:00-21:00 | Social Event drink + announcing winner |
Thursday November 7th
| 09:00-10:00 | Dennis Hendriks (TNO-ESI & RU) Synthesis-Based Engineering of Supervisory Controllers
Cyber-physical systems contain supervisory controllers that ensure the correct and safe behavior of a system. The development of such supervisory controllers becomes more and more complex, for instance due to increasing performance demands, more and more variants of the system, shortage of skilled engineers, and so on. This leads to larger development efforts and costs, and doesn’t scale towards the future. Companies need to work more efficiently, doing more with less people.State-of-the-art in engineering of supervisory controller is Synthesis-Based Engineering (SBE). It combines model-based engineering with computer-aided design. It allows engineers to focus on what the system should do (requirements) rather than how it should do it (design and implementation), raise the abstraction level, automatically synthesize correct-by-construction supervisory controllers, and develop better controllers at lower cost.By the end of the talk, you’ll know among others what SBE is, how it relates to other engineering approaches, and the current status in SBE research, tools and ecosystem. We’ll also together look at an example. Will you figure out the right control conditions? You may be surprised at how difficult it is to get the condition conditions exactly right, even for a simple example. |
| 10:00–10:30 | Coffee break |
| 10:30–11:30 | Giovanni Sileno (UvA) Normware engineering: opportunities and open problems
With the digitalization of society, the debates and the research efforts relating computational systems with regulations have been widely increasing. Yet, most arguments build upon well-established computational/formal frameworks, rather than attempting to identify more fundamental mechanisms. Aiming to go beyond this conceptual limitation, I will elaborate on taking “normware” as an explicit additional stance — complementary to software and hardware — for the interpretation and the design of artificial devices, highlighting the opportunities of a normware-centred engineering, as well as the problems it brings to the foreground. |
| 11:30–12:15 | Yuri Demchenko (UvA) Architecture and Design Aspects in Building Sustainable Digital Infrastructures for Research
Modern science is increasingly data-driven, traditionally leveraging Data Science Analytics technologies. Today, the landscape is evolving with the adoption of LLMs and Generative AI, enabling more advanced data interpretation, hypothesis generation, and predictive modeling. However, the development of scientific applications faces significant challenges in addressing energy efficiency and reduced environmental impact of both software based applications and supporting digital Research Infrastructure.This tutorial presents the results and ongoing development in the GreenDIGIT project that is focused on the architecture and design solutions to make the future digital RIs sustainable by design for achieving energy efficiency and reducing environmental impact while increasing the efficiency of the research workflows.The tutorial will introduce into the project research and development process and the proposed architecture and design solutions for scientific applications and digital infrastructure. The proposed Shared Responsibility Model for Sustainability provides a basis for defining areas of responsibility of the RI Operator and Researcher and necessary architectural and design solutions that need to be embedded in the technical RI and scientific applications design. The presented layered architecture includes both functional components to be implemented in the RI/data center and sustainability aware research development tools. The proposed solutions and recommendations are supported by the extensive analysis of the sustainability-related standards and regulations, design practices and existing software and research tools. |
| 12:30–13:30 | Lunch |
| 13:30–14:30 | Önder Babur (WUR & TU/e) Model Analytics and Intelligence
Model-Driven Engineering (MDE) promotes the use of models, metamodels and model transformations as first-class citizens to tackle the complexity of software systems. As MDE is applied for larger problems, the complexity, size and variety of those artefacts increase, as we evidence from open source and industry. With respect to model size and complexity a good amount of research has been done for handling a small number of (possibly very big and complex) models, e.g. in terms of comparison, splitting or persistence. However, scalability with respect to model variety and multiplicity (i.e. dealing with a large number of possibly heterogeneous models) has not been discussed in detail. To be able to tackle this dimension of scalability in MDE, we propose to treat the artifacts as data, and apply various techniques—ranging from statistical analysis to information retrieval and machine learning—to analyze and manage those artifacts in a holistic, scalable and efficient way. We also highlight recent work on what we believe to be the next step in MDE, where we move beyond analysis and use AI-powered techniques in MDE to support modelling, including model elicitation and extraction from natural language text, categorization and assistance. We have demonstrated our approach for a variety of model types, including metamodels, business process models, requirements models and industrial domain-specific models. |
| 14:30–15:00 | Coffee break |
| 15:00–16:00 | Justus Bogner (VU) The Challenge of Designing Green ML-Enabled Systems: A Software Architecture Perspective
While artificial intelligence (AI) and machine learning (ML) techniques are increasingly maturing, it remains very challenging for industry to develop production-ready AI-based systems and to operate and maintain them for longer periods of time. Even though ML models may only be a small piece of these systems, they nonetheless have a profound impact on their functionality and quality attributes, which can be difficult to manage. One important quality attribute that has not received the priority it deserves is environmental sustainability. In this talk, I will briefly introduce how software engineering for AI-based systems (SE4AI) has emerged to try to tackle these problems. I will then take a software architecture perspective to talk about Green AI by describing our past and ongoing efforts to synthesize and evaluate architectural tactics to improve the environmental sustainability of ML-enabled systems.About the Presenter: Dr. Justus Bogner is an Assistant Professor in Software Engineering within the Software and Sustainability (S2) group at Vrije Universiteit Amsterdam, The Netherlands. During and after his studies as well as throughout his PhD, he worked as a software engineer at Hewlett Packard and later at DXC Technology for more than nine years. After his PhD in 2020, he was a postdoctoral research scientist at the University of Stuttgart in Prof. Wagner’s Empirical Software Engineering Group for 3 years, where he led the division “Software Engineering for AI- and Microservice-Based Systems” (SE4AI&MS). His main research interests are empirical software engineering, software architecture, and software quality (maintainability, evolvability, sustainability), typically applied to AI-based systems (SE4AI) and service- and microservice-based systems. |
| 16:00–16:40 | PhD intro talks (4x) |
| 16:50–17:30 | Riemer van Rozen (CWI) Programming Languages and Games
Developing high-quality games is challenging due to the intrinsic complexity of game design. Riemer van Rozen explores how visual programming languages can empower game designers and developers with theoretical foundations, systematic approaches, and practical solutions to raise the game quality and to improve player experiences. In this talk on Programming Languages and Games, Riemer will introduce key research areas, share examples, and demonstrate tools developed over the past decade. The audience will gain insight into how interdisciplinary research can tackle critical challenges in this emerging field. |
| 18:00–19:30 | Dinner at The Market Restaurant |
Friday November 8th
| before 9:00 | check out |
| 9:00–10:00 | Olav Bunte (TU/e) Defining semantics for domain specific modelling languages
To combat the complexity of the ever growing software base, many companies have taken up modelling. These models are created using (Domain-Specific) Modelling Languages, which are designed to express the behaviour or structure of the software in a concise and clear way. Still, what the exact meaning, that is, the semantics, is of elements of these models is sometimes left to interpretation, which can differ per person. By defining the semantics precisely, only one interpretation can exist, making sure that everyone is on the same page. In this talk, I will share my experiences on the definition of the semantics of a DSML for modelling control software developed at Canon Production Printing. I will discuss multiple ways of defining semantics and give some guidelines on how to do so. Also, I will show how the semantics can be used for other purposes, such as formal verification and code generation. |
| 10:00–10:30 | Coffee break |
| 10:30–11:15 | Sander de Putter (ASML) Formal requirements verification at ASML Lithography machines are the bottleneck in nearly any semiconductor fab. Hence, to squeeze out the maximum throughput, ASML’s TwinScan minimize time spend on the critical path by utilizing its subsystemen concurrently. At the same time, to maximize availability, violations of system invariants must be avoided.
This is the main focus of ASML’s production control group.
It provides the supervisory control of the TwinScan covering high level wafer logistics and processing. The complexity of orchestrating this is immense. How can system invariants still be guaranteed to hold while the software is continuously changed?
To this end, the ASML production control group applies formal software engineering. The software is built up from smaller modules that are formally verified.
Why has ASML chosen formal software engineering? And how does ASML apply it? Find out in this talk!
|
| 11:15–12:00 | PhD intro talks (4x) |
| 12:00–12:30 | Closing and departure (with takeaway lunch) |
Registration
The registration form is available via this link Registration is closed. Registration closes on October 21 at 10:00 in the morning. However, we encourage you to register ASAP, since this will help organisation and accommodation space is limited.
Beware that if you register, but then do not participate for the period as indicated in your registration, while failing to either provide reasonable ground for this (e.g. illness, family emergency) or to cancel before the registration deadline, IPA will have to bill you for the costs incurred.
To make maximal use of the available capacity, we process applications on the following basis: Registrations are treated “first come, first served”. In principle, all PhD students (IPA and non-IPA) will share a room. Others may also be asked to share if we run out of rooms. As long as space is available and the registration deadline has not yet passed, we will accept participants.
New PhD students
PhD students new to IPA Fall Days are expected to give a brief talk in a slot of ca. 10 minutes. The purpose of such talks is to introduce your research and yourself to the IPA community. You can briefly introduce your research (research area, initial and future research directions), but also yourself (who you are, what your background is, but also e.g. you like or don’t like to do in your spare time). The Fall Days provide a friendly, open, and informal atmosphere to do this, and you will surely be welcomed into the IPA community and receive constructive feedback or get into follow-up discussions.
Venue and Travel
The Fall Days 2024 will take place at Center Parcs Park Zandvoort in Zandvoort, The Netherlands. This park is right next to the beach of the North Sea and has nice facilities such as a tropical swimming paradise. A detailed map of the park is available here. The sessions during the day take place at the business center (number 8 on the map).
The venue can easily be reached by train via the Zandvoort train station. You can plan your trip via ns.nl or 9292.nl.