Systems Verification

Course dates – HT – week beginning Monday 21st January 2019 – for Year 1 students
Daniel Kroening/Marta Kwiatkowska and Alessandro Abate

Introduction

In February 2014, Toyota has recalled 1.9 million of Prius cars due to a programming glitch in their hybrid engine system. In limited cases, the engine could shut down, causing the vehicle to stop, possibly while it is being driven. Although no incidents have been reported in this case, such design flaws can have catastrophic consequences that can be prevented by employing formal verification. The aim of systems verification is to automatically check whether a given property, for example “the car will eventually stop when the brake pedal is activated” or “the probability that the airbag fails to deploy is tolerably small”, holds for a system model, and if not provide a counterexample in the form of a trace to error. With emphasis on safety-critical systems, it can further provide correct-by-design synthesis of control actions (decisions) on the model under study. This module will give an introductory overview of the main verification techniques, including quantitative verification, which can be used to ensure the safety, reliability and efficiency of autonomous systems, supported by practical exercises and informed by case studies.

Objectives

 

  • To familiarise with the main concepts in systems modelling and property specification notations.
  • To explain the fundamentals of explicit and symbolic algorithms in qualitative and quantitative verification.
  • To gain practical experience of verification tools and how they are applied through examples of autonomous systems.
  • To give appreciation of relevant research topics in systems verification and synthesis.
Contents

 

  • Basics of verification: transition system models, temporal logics CTL and LTL, examples of system models and quantitative requirements. Fundamentals of algorithmic verification (aka model checking).
  • Basic idea of propositional satisfiability (SAT) checking, SMT solving. Bounded model checking (BMC). Unbounded verification with SAT/SMT and inductive reasoning. Application to software.
  • Introduction to quantitative verification: Markov chain models, time and rewards, probabilistic temporal logics. Overview of algorithms, including statistical model checking. Examples.
  • Quantitative verification for systems with non-determinism/decisions: Markov decision processes, issues of time and rewards, generalisation of the probabilistic temporal logic. Stochastic games if time allows. Main algorithms for verification and strategy/controller synthesis. Examples.
  • Hybrid systems. From discrete to continuous models: syntax and semantics. The role of stochasticity. Classical analysis of hybrid systems (stability, reachability). Formal abstractions for automated verification and symbolic controller synthesis. Software tools for verification and synthesis.
Prerequisites
  • Prior familiarity with logic, probability and dynamical systems (the latter two topics are covered in MT modules).
Other Sources

 

  • Principles of Model Checking, Christel Baier and Joost-Pieter Katoen, MIT Press, 2008.
  • Decision procedures, Daniel Kroening and Ofer Strichman, Springer, 2008.
  • Stochastic Model Checking (www.prismmodelchecker.org/bibitem.php?key=KNP07a), Marta Kwiatkowska, Gethin Norman and David Parker.
  • Automated Verification Techniques for Probabilistic Systems (www.prismmodelchecker.org/bibitem.php?key=FKNP11), Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman and David Parker.
  • Model Checking for Probabilistic Timed Automata (http://www.prismmodelchecker.org/bibitem.php?key=NPS13). Gethin Norman, David Parker and Jeremy Sproston. Formal Methods in System Design, 43(2), pages 164-190, Springer. September 2013
  • P. Tabuada, Verification and Control of Hybrid Systems, A symbolic approach, Springer, 2009.
  • www.prismmodelchecker.org
  • http://sourceforge.net/projects/faust2
  • https://sites.google.com/a/cyphylab.ee.ucla.edu/pessoa/home
Exercises
  • Problem sheets and practical exercises to be completed during lab sessions in the afternoon.