10.40 - 11.55

Formal methods for CPAS

Invited speaker Jana Tumová - Formal methods for dealing with road rules in autonomous driving
- abstract and bio below -

Jan Friso Groote - Designing software using mCRL2

Brayan Shali - Towards a contract theory for physical systems

Stefano Nicoletti - A Logic to Reason about Fault Trees

14.00 - 14.45

Networked control

Zhiyong Sun - Autonomous motion planning and cooperative coordination of multi-vehicle systems: addressing various constraints

Carlo Cenedese - Smart Charging of Electric Vehicle: A Game Theoretic Perspective

10.40 - 11.55

Bringing CPAS theory to industry

Twan Basten - Model-driven quality and resource management for Cyber-Physical Systems

Wilco Bonestroo - Industrial Autonomous Mobile Robots with ROS2 and Nav2

Expert panel: Bringing theory and methods for cyber-physical and autonomous systems to industrial practice
Moderator: track chair Ming Cao
Expert panel: Jan Friso Groote (TU/e), Wilco Bonestroo (Saxion), Lars De Groot (DEMCON)

14.00 - 14.45

Monitoring, detections, and fault-tolerance

Bram Ton - Insights into the invisible

Twan Keijzer - Detection of Cyber Attacks on Collaborative Systems using a Sliding Mode Observer based Approach

Lukas Miedema - Practical Fault-tolerance Against Transient Failures in Real-time DAG Scheduling

Bio Jana Tumová
Jana Tumová is an associate professor at the School of Electrical Engineering and Computer Science at KTH Royal Institute of Technology. She received PhD in computer science from Masaryk University and was awarded ACCESS postdoctoral fellowship at KTH in 2013. She was also a visiting researcher at MIT, Boston University, and Singapore-MIT Alliance for Research and Technology. Her research interests include formal methods applied in decision making, motion planning, and control of autonomous systems. Among other projects, she is a recipient of a Swedish Research Council Starting Grant to explore compositional planning for multi-agent systems under temporal logic goals and a WASP Expeditions project focusing on design of socially acceptable and correct-by-design autonomous systems.

Abstract: Formal methods for dealing with road rules in autonomous driving

Motion planning for autonomous vehicles has to be able to cope with various complex requirements from the rules of the road, presence of (dynamic) obstacles and unusual circumstances, as well as the vehicles’ own kinodynamic and geometric constraints. In this talk, we present an approach combining formal methods with traditional motion planning and control algorithms to attack this challenge. We focus on autonomous driving with rules of the road that are formalized through a temporal logic and specifically target situations where all road rules cannot be obeyed simultaneously. We introduce quantitative semantics of Linear Temporal Logic (LTL) and use robustness of Signal Temporal Logic (STL) to recognize maximally-satisfying motion plans and discuss how sampling-based algorithms can be used to compute assymptotically optimal i.e. maximally satisfying motion plans in joint planning for a fleet of autonomous vehicles and in interaction with other drivers.