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.

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