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.