International Workshop on

Formal Methods for Rigorous Systems Engineering of Cyber-Physical Systems

(co-located with CAV 2017) - Heidelberg, Germany, July 22-23, 2017

joint event with NSV 2017: 10th International Workshop on Numerical Software Verification 2017

source image:



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:

No previous knowledge of systems biology or cyber-physical systems is necessary.

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.