Deductive Verification for Stochastic Hybrid Systems

Modelling of uncertainty is an important part of the development of demonstrably safe autonomous systems. There are several sources of uncertainty including the environment with unpredictable actors; actuation and perception, whose effects cannot be exactly quantified; and the use of probabilistic algorithms to sample and analyse input data (e.g. machine learning). Whilst nondeterminism and continuous dynamics allow us to achieve models of a somewhat high fidelity, without a means to model uncertainty probabilistically an inevitable reality gap remains. Self-aware and self-managing systems, in particular, need semantics that can handle these probabilistic aspects. However, the introduction of probability further enlarges the state space, and leads to formal verification being a less tractable problem. Whilst probabilistic model checking has seen great success recently, for stochastic hybrid systems the state explosion problem motivates the need for symbolic reasoning techniques.

Deductive verification provides strong guarantees of a system's vital properties, due to its ability to handle a very large or infinite state space. This technique has successful applications for hybrid systems: a state-of-theart example is the KeYmaera X tool [2], which implements a deductive logic for verifying hybrid dynamical systems called differential dynamic logic. KeYmaera X has been successfully applied to verification of collision avoidance algorithms for autonomous and mobile robots. There is also a differential dynamic logic implementation in Isabelle/UTP [1], a verification ecosystem for Isabelle/HOL based on Unifying Theories of Programming. This implementation has the advantage of being more readily applicable to software assurance and certification, as Isabelle/HOL is a general theorem prover with facilities for code generation, which has been applied to large-scale software verification projects.

Whilst there are prototype logics for reasoning about stochastic models, such as stochastic differential dynamic logic [3], these remain unimplemented and thus unvalidated. In addition, robot models are not generally stochastic and further investigation into modelling techniques is needed. The aim of this project is to develop a verification calculus for stochastic models and an associated tool for stochastic hybrid programs in Isabelle/UTP. This could be done by extending the differential dynamic logic implementation in Isabelle/UTP to handle stochastic differential equations and random variables, which would enable the modelling of both sensor and actuator uncertainty.

The development would involve the verification of real robot controllers, which would implement behaviours using Bayesian inference methods and represent data as random variables to formalize the assumptions they make. This would both improve the confidence in the tool and yield example applications for future users. Harnessing Isabelle's code generation facilities, we will provide a method that synthesizes these behaviours into Bayesian models and provides traceability through semantic tagging from a high-level stochastic model, down to actual code for use in a simulation or physical robot platform. The use of Bayesian inference and probabilistic models is a novel application with respect to verification models that will improve the performance of real robots with uncertain data sources while ensuring explainability. We will use the York Robotics laboratory facilities and its large store of mobile robots with high-quality sensors for validation.