Correct by 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.