Correct by construction model checking

通过施工模型检查修正

• 批准号: 2598915
• 金额: --
• 依托单位: University of Strathclyde
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2598915
• 关键词: Correct; construction; model; checking

Computational systems have become ubiquitous in everyday life. Failure of those systems often leads to large-scale disruptions and incurs huge costs. Mathematics and, in particular, mathematical logic provide important tools within the area of formal verification, which aims to ensure correctness of computational systems. Abstract mathematical models are used to provide formal representations of systems and system properties are expressed in a logical language, so that these properties can be verified to hold for the system under consideration. This process of verifying a given property on an abstract model is called model-checking.While the technique of model-checking is derived from mathematical ideas, there is often a worrying gap between the underlying mathematics and the actual verification algorithms. Implementations are often ad-hoc and written in programming languages that provide only limited support for ensuring correctness. Therefore, there are insufficient guarantees that the verification software itself is working correctly. The central goal of this project is to close this gap by developing mathematical techniques that allow the extraction of algorithms that are correct by construction: by extracting the algorithm from a proof that the specification can be fulfilled, it is guaranteed to fulfil it. By basing our work on and extending the rich mathematical framework of category theory and coalgebra, we will in addition ensure that our model-checking algorithms will be able to verify different types of systems with various verification concerns involving costs, resources and probabilities.

计算系统在日常生活中已经无处不在。这些系统的故障通常会导致大规模的中断并带来巨大的成本。数学，特别是数理逻辑在形式验证领域提供了重要工具，旨在确保计算系统的正确性。抽象数学模型用于提供系统的形式表示，并且系统属性以逻辑语言表达，以便可以验证这些属性是否适用于所考虑的系统。在抽象模型上验证给定属性的过程称为模型检查。虽然模型检查技术源自数学思想，但基础数学与实际验证算法之间常常存在令人担忧的差距。实现通常是临时的，并且用编程语言编写，只为确保正确性提供有限的支持。因此，不足以保证验证软件本身正常工作。该项目的中心目标是通过开发数学技术来缩小这一差距，这些技术允许提取通过构造正确的算法：通过从可以满足规范的证明中提取算法，保证满足它。通过基于范畴论和余代数丰富的数学框架并扩展我们的工作，我们还将确保我们的模型检查算法能够验证不同类型的系统，并具有涉及成本、资源和概率的各种验证问题。