Deductive Verification for Stochastic Hybrid Systems

随机混合系统的演绎验证

• 批准号: 2605387
• 金额: --
• 依托单位: University of York
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2605387
• 关键词: Deductive; Verification; 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.

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