Program

Overview

	23 October 2019 (Wednesday)
09:00-09:30	Registration
09:30-10:30	Keynote: Carlo Ghezzi
10:30-11:00	Coffee
11:00-12:30	Session 1
12:30-14:00	Lunch (at Polder)
14:00-15:15	Session 2
15:15-15:45	Coffee
15:45-17:30	Tutorial: Jan Friso Groote & Tim Willemse
17:30-19:00	Drinks
	24 October 2019 (Thursday)
09:30-10:30	Keynote: Kim Larsen
10:30-11:00	Coffee
11:00-12:30	Session 3
12:30-14:00	Lunch
13:00-14:00	SC meeting
14:00-…	Social event
	25 October 2019 (Friday)
09:30-10:30	Keynote: Wan Fokkink
10:30-11:00	Coffee
11:00-12:30	Session 4
12:30-14:00	Lunch (at Polder)
14:00-15:30	Session 5

Keynote: Carlo Ghezzi

Title: Software engineering for cyber-physical spaces

Abstract: Computing and communication capabilities are increasingly being embedded into physical spaces, blurring the boundary between computational and physical worlds. Typically, this is the case of modern cyber-physical or internet-of-things (IoT) systems implementing smart spaces, ranging from smart homes and offices to smart cities. Collectively, these systems may be called cyber-physical spaces (CPSp’s). The talk focuses on design and operation of CPSp’s, discussing how software engineering concepts — abstraction, modeling, and verification —  can contribute to their design and operation. Conceptually, such composite environments can be abstracted into a topological model where computational and physical entities are connected in a graph structure. Like most modern software-intensive system, CPSp’s are highly dynamic and typically undergo continuous change –- they are evolving. Modeling space and its dynamics, as well as supporting formal reasoning about various properties of an evolving space, are crucial prerequisites for engineering dependable space-intensive systems.
This talk will show an avenue for research which can be characterized as rethinking spatial environments from a software engineering perspective — in both design and operation aspects. Regarding design, it shows how domain descriptions can give rise to models amenable to automated analyses of dynamic behaviors in spaces populated by humans, robots, and mobile devices. Verification amounts to assessing if some collective behaviors violate certain requirements the overall system should exhibit. In particular, the talk will discuss how verification can scale to realistic space models. Regarding runtime, it will consider supporting analyses on the cloud on behalf of resource-constrained and spatially-distributed IoT devices. It will hint at how spatial  verification processes can be integrated in the service layer of an IoT-cloud architecture based on microservices, and what tradeoffs emerge across different deployment options. 

About: Carlo Ghezzi is professor of Software Engineering at Polytechnic University of Milan. His research interests include “methods and tools to improve dependability of adaptable and evolvable distributed applications, such as service-oriented architectures and ubiquitous/pervasive computer applications.” Ghezzi is distinguished member of several societies (ACM Fellow; IEEE Fellow; Academia Europaea), he won an ACM SIGSOFT Outstanding Research Award, and he received an ERC Advanced Grant.

Keynote: Kim Larsen

Title: Compositional Verification and Testing of Real-Time Systems

Abstract: In this talk we present a tool supported framework for compositional verification of real-time systems. The framework used Timed I/O Automata (TIOA) as specifications and implementations with a satisfaction relation, a refinement relation and a  set of operators supporting stepwise refinement.  In particular, the framework comes equipped with algorithms for refinement and consistency checking as well as constructs for logical, parallel composition and quotienting, all indispensable ingredients of a compositional design methodology. In fact the framework has all the necessary constructs to support assume-guarantee reasoning about designs.

About: Kim Larsen is professor of Computer Science at Aalborg University. His research interests include “modeling, verification, performance analysis of real-time and embedded systems with applications to concurrency theory and model checking,” and he is the driving force behind the UPPAAL verification tool. Larsen heads multiple research centers on embedded and cyber-physical systems, he received an ERC Advanced Grant, and his work has over 26K citations.

Keynote: Wan Fokkink

Title: Putting Supervisory Control Synthesis to Work

Abstract: Supervisory Control Theory, initiated by Ramadge-Wonham, turns out to be very suitable for designing and generating software for the control of large infrastructural systems like bridges, locks and tunnels. In this talk recent research results will be discussed that were pivotal in tackling such large applications, including multilevel synthesis, determining a control problem dependency graph, and several modeling guidelines.

About: Wan Fokkink is professor of Theoretical Computer Science at Vrije Universiteit Amsterdam and professor of Model Based System Engineering at Eindhoven University of Technology. His research interests include “analysis and design of distributed systems, broadly construed, ranging from automatically synthesizing control software to formal verification of communication protocols and executable models of biological systems.” Fokkink has written several textbooks on process algebra and distributed algorithms, he co-founded IFIP Working Group 1.8 on Concurrency Theory, and he published 150+ peer-reviewed articles.

Tutorial: Jan Friso Groote & Tim Willemse

Title: Modelling and Analysis of Communicating Systems Using mCRL2

Abstract: Parallel programs and distributed, communicating systems become increasingly common. This is driven by the fact performance improvement is mainly to be expected from exploiting multiple computing cores. However, designing parallel and distributed systems that are correct is notoriously difficult. The mCRL2 toolset is designed to reason about such systems. Its modelling language is based on a rich, ACP-style process algebra and has an axiomatic view on processes. The data theory is based on the theory of abstract data types (ADTs). The language for expressing requirements of systems is based on a first-order extension of the modal mu calculus.
In this tutorial we give an overview of the languages, theories and techniques that are used in the mCRL2 toolset. We address, among others, the theory and application of behavioural equivalences and preorders, and the theory and application of modal formulae for carrying out an analysis of the correctness of parallel and communicating systems. Time permitting, we will discuss the recently added support for modelling and analysing probabilistic processes.

About: Jan Friso Groote is professor of Formal System Analysis at Eindhoven University of Technology. His research interests include “computer systems, architectures, networks, software, algorithms, control systems, embedded systems and formal methods.” Groote is the founder of the mCRL2 analysis toolset, he co-authored the mCRL2 book, and he collaborates with industry (e.g., ASML, Verum) to verify real software systems.
Tim Willemse is associate professor at Eindhoven University of Technology. His research interests include “algorithms and theory for PBES, parity games and model-based testing theories, and applications of model checking.” Willemse is a core contributor of mCRL2, he is an expert on PBES (which drives MCRL2’s verification technology), and he led the team that verified control software of CERN’s Large Hadron Collider using mCRL2.

Accepted Papers

Session 1

• Announcements: opening

• Timm Liebrenz, Paula Herber and Sabine Glesner: A Service-oriented Approach for Decomposing and Verifying Hybrid System Models (45 min. + nominee best paper award)

• Habtom Kahsay Gidey, Alexander Collins and Diego Marmsoler: Modeling and Verifying Dynamic Architectures with FACTum Studio (30 min.)

Session 2

• Petra van den Bos and Frits Vaandrager: State Identification for Labeled Transition Systems with Inputs and Outputs (45 min. + nominee best paper award)

• Peter Zeller, Annette Bieniusa and Arnd Poetzsch-Heffter: Combining state- and event-based semantics to verify highly available programs (30 min.)

Session 3

• Kadir Bulut, Guy-Vincent Jourdan and Uraz Cengiz Turker: Minimizing characterizing sets: hardness and effect on test derivation from systems modelled as finite state machines (45 min. + nominee best paper award)

• Lars Luthmann, Hendrik Göttmann and Malte Lochau: Compositional Liveness-Preserving Conformance Testing of Timed I/O Automata (30 min.)

• Announcements: social event logistics

Session 4

• Achim D. Brucker and Michael Herzberg: A Formally Verified Model of Web Components (30 min.)

• Reynaldo Cobos Mendez, Julio de Oliveira Filho, Douwe Dresscher and Jan Broenink: A Bond-graph Metamodel: Physics-based Interconnection of Software Components (30 min.)

• Arpit Sharma: Revisiting Trace Equivalences For Markov Automata (30 min.)

Session 5

• Tobias Reiher, Alexander Senier, Jeronimo Castrillon and Thorsten Strufe: RecordFlux: Formal Message Specification and Generation of Verifiable Binary Parsers (30 min.)

• Kasper Dokter: Multilabeled Petri Nets (30 min.)

• Christopher Esterhuyse and Hans-Dieter Hiep: Reowolf: Synchronous Multi-Party Communication over the Internet (30 min.)

Social Event

• We leave CWI at 14:00.
• We take the 14:28 train from station Amsterdam Science Park to station Amsterdam Centraal.
• We take a 15-minute walk from Amsterdam Centraal to Cafe Papeneiland (address: Prinsengracht 2); you can also meet us here directly instead of joining from CWI.
• At 15:00, we embark on a 4-hour tour “to find out everything there is to know about Amsterdam and Dutch cuisine“ (excellent reviews on TripAdvisor).
• In the words of the tour operator: “At no less than 8 food stops we will treat you to all the classics, including herring, Gouda cheese, bitterballen and authentic Dutch apple pie (appeltaart) and we will add a little spice from the east with a taste of the Indonesian ‘rijsttafel’. Take your pick of the locally brewed artisan beers or you might want to try one of the many Dutch ‘jenevers’ (gins). We will tell you about Amsterdam’s early beginnings and how, in the 17^th century, this city was able to expand to one of the most powerful and, without a doubt, most beautiful cities of the world. It will come as no surprise to you that our food history was significantly influenced by this development. We will stay clear of the crowded inner-city and show you the beauty and tranquility of the 17^th-century Jordaan with it’s quant houses, many colorful flower baskets and tree-shaded canals. But amidst all this glorious history we do not forget to show you the splendor of present-day Amsterdam. We will introduce you and your fellow to its local residents and our ‘food heroes’, the small local businesses who provide us with their superb food.”
• Around 19:00, the tour ends in Cafe De Twee Zwaantjes (address: Prinsengracht 114; near the tour’s starting point). The tour should provide enough food for the rest of the night..!
• We can give custom advise on how to get back to your hotels from the city center; we have not arranged a group return to CWI, as CWI is in the wrong direction for most hotels.