(The program is preliminary.)


23 October 2019 (Wednesday)
Keynote: Carlo Ghezzi
11:00-12:30Session 1
12:30-14:00Lunch (at Polder)
14:00-15:15Session 2
15:45-17:30Tutorial: Jan Friso Groote & Tim Willemse
24 October 2019 (Thursday)
09:30-10:30Keynote: Kim Larsen
11:00-12:30Session 3
13:00-14:00SC meeting
14:00-…Social event
25 October 2019 (Friday)
09:30-10:30Keynote: Wan Fokkink
11:00-12:30Session 4
12:30-14:00Lunch (at Polder)
14:00-15:30Session 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: TBA

Abstract: TBA

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: TBA

Abstract: TBA

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: TBA

Abstract: TBA

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.)