Description
Conventional real-time embedded systems have over the past two decades vividly evolved into an open, interconnected form, now known as cyber-physical systems (CPS), that integrates capabilities of computing, communication and control, thereby triggering yet another round of global revolution of the information technology. The underlying safety-critical feature, however, impels the community to tackle the grand challenge concerning analysis, verification and design of reliable CPS. Hybrid systems that seamlessly integrate continuous dynamics with discrete behaviors have been extensively used as mathematical models for CPS, wherein prominent formal techniques, e.g., reachability-based model checking, deduction-based theorem proving and correct-by-construction synthesis, have been developed for ensuring correctness of hybrid systems. In this tutorial, we will start with a lightweight introduction to CPS and hybrid systems in a safety-critical context and then present our efforts over the recent years in testing, verification and design of CPS, particularly addressing inherent features thereof like large-scale, nondeterminism and delayed coupling.The tutorial is scheduled in three sessions. The first session sketches an overview of formal verification of CPS and Hybrid Automata (HA) as the model for hybrid systems underneath, followed by path-oriented/enumeration techniques addressing bounded model checking of complex HA while tackling nondeterminism therein with an online modelling and verification framework. In the second session, we show how to use proper design patterns to simplify HA verification and contrarily how to exploit HA to assist testing of real-time CPS. We dedicate the third session to the verification and design of time-delayed systems ubiquitously existing in networked and distributed control. We present various approaches to the automatic verification and correct-by-construction design of dynamical systems subject to delayed information exchange, with applications in a typical set of time-delayed dynamics originated from realms of biology, control and transportation.
| Period | 1 Dec 2020 |
|---|---|
| Event title | The 41st IEEE Real-Time Systems Symposium: Hot Topics Day |
| Event type | Conference |
| Conference number | 2020 |
| Degree of Recognition | International |