Deductive Verification for Stochastic Hybrid Systems

不确定性建模是开发可论证安全自主系统的重要组成部分。不确定性有几个来源，包括具有不可预测行为者的环境；驱动和感知，其影响无法精确量化；以及使用概率算法对输入数据进行采样和分析（例如机器学习）。虽然不确定性和连续动力学使我们能够实现某种程度上高保真度的模型，但如果没有一种方法来模拟不确定性，不可避免的现实差距仍然存在。自我意识和自我管理系统尤其需要能够处理这些概率方面的语义。然而，概率的引入进一步扩大了状态空间，导致形式验证成为一个难以处理的问题。虽然概率模型检验近年来取得了巨大的成功，但对于随机混合系统，状态爆炸问题激发了对符号推理技术的需求。演绎验证为系统的重要属性提供了强有力的保证，因为它能够处理非常大或无限的状态空间。该技术已成功应用于混合动力系统：KeYmaera X工具[2]就是一个最先进的例子，它实现了一种用于验证混合动力系统的演绎逻辑，称为差分动态逻辑。KeYmaera X已成功应用于自主和移动机器人的避碰算法验证。在Isabelle/UTP[1]中也有一个差分动态逻辑实现，这是一个基于统一编程理论的Isabelle/HOL验证生态系统。这种实现的优点是更容易适用于软件保证和认证，因为Isabelle/HOL是一个具有代码生成功能的一般定理证明器，它已应用于大型软件验证项目。虽然存在用于随机模型推理的原型逻辑，例如随机微分动态逻辑[3]，但这些仍然未实现，因此未经验证。此外，机器人模型通常不是随机的，需要进一步研究建模技术。本项目的目的是为Isabelle/UTP的随机混合程序开发一种验证演算和相关工具。这可以通过扩展Isabelle/UTP中的微分动态逻辑实现来处理随机微分方程和随机变量，这将使传感器和执行器的不确定性建模成为可能。该开发将涉及对真实机器人控制器的验证，该控制器将使用贝叶斯推理方法实现行为，并将数据表示为随机变量以形式化他们所做的假设。这既可以提高对该工具的信心，又可以为将来的用户提供示例应用程序。利用Isabelle的代码生成工具，我们将提供一种方法，将这些行为综合到贝叶斯模型中，并通过语义标记从高级随机模型提供可追溯性，直到在仿真或物理机器人平台中使用的实际代码。贝叶斯推理和概率模型的使用是验证模型的一种新应用，它将在确保可解释性的同时提高具有不确定数据源的真实机器人的性能。我们将使用约克机器人实验室设施及其大量具有高质量传感器的移动机器人进行验证。

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.