Ana Cavalcanti (University of York) is Professor of Software Verification and Royal Academy of Engineering Chair
in Emerging Technologies working on Software Engineering for Robotics: modelling, validation, simulation, and testing.
She currently leads the RoboStar research group at the University of York. She held a Royal Society-Wolfson Research
Merit Award and a Royal Society Industry Fellowship to work with QinetiQ in avionics. She has chaired the Programme
Committee of various well-established international conferences, is on the editorial board of four international
journals, and is Chair of the board of the Formal Methods Europe Association. Her current research is on theory
and practice of verification and testing for robotics.
Simulation is favored by roboticists to evaluate controller design and software. Often, state machines are drawn to convey overall ideas and used as a basis to program tool-specific simulations. The simulation code, written in general or proprietary programming languages, is, however, the only full account of the robotic system. In this course, we present the RoboStar technology, a modern approach to design that supports automatic generation of simulation code guaranteed to be correct with respect to a design model, and complements simulation with model checking, theorem proving, and automatic test generation for simulation. Diagrammatic domain-specific, but tool-independent, notations for design and simulation use state machines, differential equations, and controlled English to specify behavior. This course will be co-lectured by James Baxter , Gustavo Carvalho , Alvaro Miyazawa , Pedro Ribeiro and Matt Windsor from University of York.
Jim Woodcock FREng is the Professor of Software Engineering at the University of York. He holds two additional
posts: he is a Professor of Digital Twins at Aarhus University in Denmark and a 1,000-talents Professor of
Cyber-Physical Systems (CPS) at Southwest University in Chongqing. He is an award-winning researcher with
40 years' experience in formal methods for software engineering. He has widely cited theoretical work in
efficient verification algorithms for security and in more general software and hardware semantics. His work
has been widely used in practice. He is a long-term consultant to the UK government on system security
verification, including co-authoring a secure office automation system for the UK government. He created
the theory and practical verification for NatWest Bank's Mondex smart-card system, the first commercial
product to achieve ITSEC Level E6 (Common Criteria EAL 7). He has made significant contributions to the
Verified Software Initiative. He was a principal investigator in the EU FP7 COMPASS project on model-based
systems of systems and in the EU H2020 INTO-CPS project on integrated toolchains for CPS. He currently leads
the research team in York for the Verifiability Research Node in the EPSRC Trusted Autonomous Systems
Programme. For the last decade, he has researched the theory and practice of CPS and, more recently,
verified robotics and digital twins. He leads the research team that is developing theories for modelling
and verifying CPS and robotics using the Isabelle/UTP theorem prover. Jim is a fellow of the UK Royal
Academy of Engineering and a Chartered Engineer. He has served as head of the Department of Computer
Science in York.
The course consists of three sessions. Each session consists of three 1-hour lectures.
Dr. Xin Chen is an assistant professor in the Department of Computer Science at the University of
Dayton. He received his Ph.D. in Computer Science from RWTH Aachen University in 2015, and was a
postdoctoral research associate at the University of Colorado Boulder. Dr. Chen is primarily
interested in developing both model-based and model-free techniques for safety verification and
resilient control of autonomous systems. He is the primary developer of the CPS formal verification
tool Flow*. His research work is funded by the U.S. Air Force Research Laboratory.
Formal verification of Cyber-Physical Systems (CPS) has been a significant research topic due to the increasing use of computer controlled systems in safety-critical areas, such as power systems, medical devices and autonomous vehicles. However, such tasks are often very difficult because of the complicated behavior of CPS. Reachability analysis is an effective way to formally prove the safety of a CPS over a bounded or unbounded time horizon. A reachability analysis approach computes an overapproximation of the reachable set and verifies whether there is any unsafe state included. If not, then the system is safe. The main challenge of computing a valid reachable set overapproximation is to control the growth of overapproximation error which is also called overestimation.
This course focuses on the reachability analysis of an important class of learning-enabled CPS which are called Neural Network Controlled Systems (NNCS). We present a polynomial arithmetic-based framework named POLAR for computing higher-order overapproximate reachable sets for NNCS. We progressively teach the techniques by describing (1) the existing set-based computation methods and functional overapproximation forms such as Taylor models, (2) the Taylor model-based verification techniques for nonlinear hybrid systems, (3) functional overapproximation for feedforward neural networks and its use in computing accurate reachable sets for NNCS. Besides, a short course of using Flow* and POLAR will also be provided.
