source image: https://de.wikipedia.org/
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
Techniques and Tools for Hybrid Systems Reachability Analysis
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.
ProbReach: Probabilistic Bounded Reachability for Uncertain Hybrid Systems
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.
- introduction to delta-satisfiability and delta-complete decision procedures;
- probabilistic bounded delta-reachability;
- ProbReach tool demo.
Road to safe autonomy with data and formal reasoning
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.
CounterExample Guided Synthesis of Sound Controllers for Cyber-Physical Systems with SAT Solvers
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.