Lectures Introduction

Prof. Ana Cavalcanti

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.

RoboStar framework for design and verification of robotic systems

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.

Prof. Jim Woodcock

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.

An introduction to modelling and verification in Isabelle/HOL

The course consists of three sessions. Each session consists of three 1-hour lectures.

  • Session 1 Introduction to Isabelle:
    • Getting started with Isabelle/HOL.
    • Functional programming in Isabelle.
    • Isar: intelligible semi-automated reasoning.
  • Session 2 Logic and mathematical data types in Isabelle:
    • Natural deduction.
    • Predicate quantifiers.
    • Sets and functions.
  • Session 3 Specification and Verification in Isabelle:
    • Automation and Sledgehammer.
    • Tacticals.
    • ZMachines: specification and animation.

Prof. Xin Chen

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.

Functional Overapproximation for Reachability Analysis of Neural Network Control Systems

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.