source image: https://de.wikipedia.org/

Organizer

• Ezio Bartocci, TU Wien, Austria

Objectives

Cyber-Physical Systems are engineering, physical and biological systems whose operations are integrated, monitored, and/or controlled by a computational core. CPS are increasingly employed as models for a variety of processes ranging from biological (e.g., cardiac cells, genetic regulatory networks) to engineered (e.g., networked mobility, smart grids, smart factories, smart health care). CPS are spatially distributed, and their behaviour results from the nonlinear (often stochastic) interaction between discrete and continuous phenomena. As the complexity of these systems increases, so does the range of spatial and temporal emergent behavioural properties that they can exhibit. As a consequence, a major research challenge is to devise tools and techniques for the efficient monitoring and prediction of such behaviours, in addition to develop design techniques for the automatic optimisation and adaptation of CPS to meet the desired temporal and spatial requirements.

This workshop is sponsored by the Austrian Society for Rigorous Systems Engineering (RiSE) and it aims to invite international world-renown researchers in the field of formal methods to to provide tutorials on computational tools for the design and the automated analysis of complex CPS and to foster potential collaborations of the workshop’s participants within the RISE network.

Tutorial #1
Techniques and Tools for Hybrid Systems Reachability Analysis

Erika Abraham, RWTH Aachen University, Germany

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 techniques for the safety analysis of hybrid systems using SMT solving. Currently she is professor at RWTH Aachen University (Germany), with main research focus on formal methods for hybrid and probabilistic systems, and SMT solving for real and integer arithmetic.

In this talk we give an overview of reachability analysis techniques for hybrid systems with mixed discrete-continuous behaviour. We focus on a certain type of algorithms which over-approximate the set of states that are reachable in a given hybrid system by iteratively over-approximating successors of state sets. After discussing theoretical aspects, we shortly describe available tools and introduce in more detail our HyPro library, explain its functionalities, and give some examples to demonstrate its strengths and weaknesses.

Tutorial #2
ProbReach: Probabilistic Bounded Reachability for Uncertain Hybrid Systems

Fedor Shmarov and Paolo Zuliani, Newcastle University, UK

Fedor Shmarov received his BSc in Information Science and Computer Technology from Tambov State Technical University in 2011, and his MSc in Advanced Computing Science from Newcastle University in 2013. Currently, he is a final year PhD student under the supervision of Dr. Paolo Zuliani in the School of Computing Science at Newcastle University. His main area of interests are formal methods and model checking. His PhD project involves verification of cyber-physical systems, where he develops techniques for verification of systems with stochastic and nondeterministic behaviour.

Dr. Paolo Zuliani is a Lecturer (Assistant Professor) in the School of Computing Science at Newcastle University, UK. He received his Laurea degree in computer science from Universita' degli Studi di Milano, Italy, and his DPhil in computer science from the University of Oxford, UK. Dr. Zuliani's expertise lies largely in formal methods for reasoning about computing systems, with an emphasis on probabilistic and quantum systems. He is in particular interested in the verification of biological systems, cyber-physical systems, and quantum programs.

We give an overview of our recent work on verified probabilistic reachability for hybrid systems with uncertain parameters. Essentially, the problem reduces to computing validated enclosures for reachability probabilities. We present two approaches: one has high computational cost and provides absolute guarantees on the correctness of the answers, i.e., the computed enclosures are formally guaranteed to contain the reachability probabilities. The other approach combines rigorous and statistical reasoning, thereby yielding better scalability by trading absolute (formal) guarantees with statistical guarantees. We exemplify both approaches with case studies from systems biology and cyber-physical systems.

The tutorial is divided into three parts:

• introduction to delta-satisfiability and delta-complete decision procedures;
• probabilistic bounded delta-reachability;
• ProbReach tool demo.

Tutorial #3
Road to safe autonomy with data and formal reasoning

Sayan Mitra, University of Illinois at Urbana-Champaign, USA

Sayan Mitra is an Associate Professor of Electrical and Computer Engineering. His research interests include formal methods, distributed computing, and mathematics for rigorous engineering of systems. He holds a PhD from MIT (2007), MSc from the IISc, Bangalore, and undergraduate degree from Jadavpur University, Kolkata. He was a postdoctoral fellow at CalTech, and has held visiting faculty positions at Oxford University, Air Force Research Laboratory (Kirkland), and TU Vienna. Sayan received the National Science Foundation's CAREER Award, AFOSR Young Investigator Research Program Award, IEEE-HKN C. Holmes MacDonald Outstanding Teaching Award, Samsung Global Research Outreach Award, and several best paper awards.

We present an overview of recently developed data-driven tools C2E2 and DryVR for safety analysis of autonomous cyber-physical systems, specifically advanced driver assist systems. The core algorithms combine model-based, hybrid system reachability analysis with sensitivity analysis of components with possibly unknown, complex, or inaccessible models. We illustrate the applicability of this approach in several case studies emergency braking systems, merging vehicles, and engine control systems. We show that the data-driven verification tool can effectively prove the safety of certain scenarios, and also compute the severity of accidents for unsafe scenarios.

Tutorial #4
CounterExample Guided Synthesis of Sound Controllers for Cyber-Physical Systems with SAT Solvers

Alessandro Abate, University of Oxford, UK

Alessandro Abate is an Associate Professor in the Department of Computer Science at the University of Oxford. He received a Laurea degree in Electrical Engineering (summa cum laude) in October 2002 from the University of Padova. As an undergraduate he also studied at UC Berkeley and RWTH Aachen. He earned an MS in May 2004 and a PhD in December 2007, both in Electrical Engineering and Computer Sciences, at UC Berkeley, working on Systems and Control Theory with S. Sastry. Meanwhile he was an International Fellow in the CS Lab at SRI International in Menlo Park (CA). Thereafter, he has been a PostDoctoral Researcher at Stanford University, in the Department of Aeronautics and Astronautics, working with C. Tomlin on Systems Biology in affiliation with the Stanford School of Medicine. From June 2009 to mid 2013 he has been an Assistant Professor at the Delft Center for Systems and Control, TU Delft - Delft University of Technology, working with his research group on Verification and Synthesis over complex systems and on Systems Biology.

We consider a classical model setup for Cyber-Physical Systems, comprising a physical plant represented as a linear, time-invariant model, which is closed loop with a digitally-implemented controller. As a key CPS feature, the plant model is given as a dynamical equation with inputs, evolving over a continuous state space, whereas the control signals are discrete in time and value. The goal is to design a controller with a linear architecture ensuring that the closed-loop plant is safe, and at the same time accounting for errors due to the signals digitalisation, the manipulation of quantities represented with finite word length, and finally possible imprecisions in the description of the plant model. We present a sound and automated approach based on counterexample guided inductive synthesis (CEGIS). The CEGIS architecture encompasses two phases: a synthesis step and a verification phase. We first synthesise a feedback controller that stabilises the plant but that may not be safe; safety is thereafter verified either via BMC or abstract acceleration. If the verification step fails, a counterexample is provided to the synthesis engine and the process iterates. We demonstrate the practical value of this new CEGIS-based approach by automatically synthesising digital controllers for numerous models of physical plants extracted from the control literature.