Tutorial T2

Title: Taming Delays in Cyber-Physical Systems

Abstract: The advent of systems of cooperative cyber-physical systems draws attention to a central problem of networked and distributed control systems: the ubiquity of delay in feedback loops between logically or spatially distributed components, which is not adequately re ected in traditional models of hybrid-state dynamics based on ordinary differential equations and immediate transitions. The occurrence of feedback delays may significantly alter a system’s dynamic response. Unmodelled delays in a control loop consequently have the potential to invalidate any stability or safety certificate obtained on a related delay-free model, which is the current practice in hybrid- system analysis. In this tutorial, we will present various approaches to the analysis and correct-by-construction design of dynamical systems subject to delayed information exchange, as pertinent to distributed hybrid systems. We will explain automatic verification procedures for invariance properties over bounded or unbounded temporal horizons. This analytical view will be complemented by a constructive one for synthesizing delay-resilient control strategies for discrete and hybrid discrete-continuous dynamics.

Motivation

Conventional embedded systems have over the past decades vividly evolved into an open, interconnected form that integrates capabilities of computing, communication, and control, thereby triggering yet another round of global revolution of the information technology. This form, now known as cyber-physical systems (CPS), has witnessed an increasing number of safety-critical systems particularly in major scientific projects vital to people’s livelihood. Prominent examples include automotive electronics, health care, nuclear reactors, high-speed transportations, manned space ight, etc., in which a malfunction of any software or hardware component would potentially lead to catastrophic consequences like significant casualties and economic losses. Meanwhile with the rapid development of feedback control, sensor techniques, and computer control, time delays have become an essential feature underlying both the continuous evolution of physical plants and the discrete transition of computer programs, which may well annihilate the stability/safety certificate and control performance of embedded systems. Traditional engineering methods, e.g., testing and simulations, are nevertheless argued insufficient for the zero-tolerance of failures incurred in time-delayed systems in a safety-critical context. Therefore, how to rigorously verify and design reliable safety-critical embedded systems involving delays tends to be a grand challenge in the computer science and control theory community.

In contrast to delay-free systems, time-delayed systems yield substantially higher theoretical complexity thus rendering the underlying design and verification tasks exceedingly harder. This tutorial focuses on formal modelling, verification, and control synthesis of time-delayed, networked hybrid systems, while particularly addressing the stability/safety verification of continuous dynamics governed by delay differential equations (DDEs), the control-strategy synthesis of discrete dynamics captured by delayed safety games, and the switching-logic synthesis of hybrid dynamics modelled as delay hybrid automata, with applications in a typical set of time-delayed dynamics originated from realms of biology, control, astronautics, and transportation.

Though time delays have been extensively studied in the literature of mathematics and control theory from a qualitative perspective, automatic verification and synthesis methods addressing feedback delays in hybrid discrete-continuous systems are still in their infancy. This tutorial delivers a peek into the blueprint of hybrid systems under delays, wherein the attendees will grasp quantitative techniques, e.g., interval Taylor models, validated simulations, sensitivity analysis, linearization, spectral analysis, and invariant generation, and thereby learn how to achieve formal verification and synthesis of time-delayed systems leveraging these commonly used ingredients in the community of formal methods. With plenty of illustrating examples provided throughout the tutorial, the attendees may realize how to make mathematical techniques contribute to real-world applications, and hopefully, be inspired by the success stories on verification and synthesis of time-delayed dynamics presented in this tutorial and start to use the proposed approaches, or even develop their own formal methods, for their future work.

Form of the Tutorial

This tutorial will be delivered as a half-day, lecture-style event, possibly with hands-on demonstrations of the corresponding tools. The tutorial is intended for audiences with general interests in the modelling, analysis, verification, and design of embedded systems, ranging from bachelor/graduate students to senior researchers in the community. We plan to deliver the tutorial virtually via Zoom while providing necessary software repositories through GitHub; the attendees will interact with the instructors in small groups by means of breakout rooms in Zoom.
Part of this tutorial has been offered previously at RTSS 2020 (December 1, 2020) in a virtual format (pre-recorded videos combined with live Q&A sessions), with approximately 30 attendees then. This tutorial includes significantly new results obtained thereafter, e.g., switching-logic synthesis of hybrid dynamics modelled as delay hybrid automata, synthesis of (control) barrier-certificate functionals for DDEs with inputs and disturbances, etc.

List of Topics
  • An overview of CPS and hybrid systems featuring networked delays, in particular, delay hybrid automata, which augment classical hybrid automata with time delays in both discrete jumps and the continuous evolution.
  • Verifying stability/safety of delayed differential dynamics possibly with inputs and disturbances:
    • bounded verification based on validated simulations and the boundary propagation of reachable sets;
    • unbounded verification via interval Taylor models, spectral analysis plus linearization, and control barrier-certificate functional synthesis.
  • Synthesizing safe controllers resilient to time delays:
    • for discrete dynamics:
      • safety games played under discrete delays and their decidability of controllability,
      • incremental synthesis of delay-resilient control strategies,
      • equivalence of qualitative controllability for safety games under different delay patterns;
    • for hybrid discrete-continuous dynamics:
      • local invariant generation for DDEs based on reachable-set computation,
      • global invariant generation for delayed hybrid dynamics based on fixed-point computation,
      • safe switching-logic synthesis for delayed hybrid dynamics based on invariant generation.

The above topics cover our recent results published at IEEE Trans. Automat. Contr., Acta Informatica, CAV, FM, HSCC, CDC, ATVA, FORMATS, etc.

Biographies of the Instructors

Dr. Naijun Zhan is a distinguished professor at the State Key Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China. He received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences in 2000, and M.Sc. in computer science and B.Sc in mathematics both from Nanjing University respectively in 1996 and 1993. Prior to joining the Institute of Software, he was a Research Fellow with the Faculty of Mathematics and Information, University of Mannheim, Mannheim, Germany, from 2001 to 2004. His research interests include formal techniques for the design of real-time and hybrid systems, program verification, and modal/temporal logics. He has published two books and more than one hundred papers in the leading international journals and conferences. He is a member of the editorial boards of Formal Aspects of Computing and Journal of Logical and Algebraic Methods in Programming; PC co-chair of FM 2021 and other conferences; and serves in the program committees of CAV, RTSS, HSCC, EMSOFT, HSCC, ICCPS, etc.

Dr. Mingshuai Chen is a postdoctoral researcher at the Chair for Software Modeling and Verification, Department of Computer Science, RWTH Aachen University, Aachen, Germany. He received his Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences in 2019, and B.Sc. in computer science from the School of Computer Science and Technology, Jilin University in 2013. His main research interest lies in the formal verification and synthesis of programs and hybrid systems for ensuring the reliability and effectiveness of safety-critical cyber-physical systems. He has published over twenty peer-reviewed papers at agship journals/conferences including IEEE Trans. Automat. Contr., Acta Informatica, CAV, TACAS, IJGAR/CADE, FM, etc. He serves in the reviewer panel of AMS Mathematical Reviews and the program/repeatability committees of RTCSA, ADHS, VMCAI, SYNASC, etc. He was the awardee of the Distinguished Paper Award at ATVA 2018, Best Paper Award at FMAC 2019, and the CAS-President Special Award in 2019.