MEBI: Mechanised Bisimilarities and Behavioural-typed Processes

MEBI：机械化的相似性和行为类型的过程

• 批准号: EP/Y00339X/1
• 负责人: David Castro-Perez
• 金额: $ 20.68万
• 依托单位: University of Kent
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2024
• 资助国家: 英国
• 起止时间: 2024 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FY00339X%2F1
• 关键词: MEBI; Mechanised; Bisimilarities; Behavioural; typed

Building correct communicating systems (i.e. concurrent and distributed systems) is a hard task. Such systems often present non-deterministic behaviours that are hard to reproduce. This means that, whenever there is a bug in one of such systems, fixing it is a time consuming and costly task. Furthermore, distributed systems are nowadays widespread in our society, including key sectors such as banking or E-healthcare. Thus, bugs in communicating systems can be very damaging, threatening large economic costs, and the safety and security of the industries that rely on them.To guarantee the correctness of communicating systems, many tools and theories have been developed. Session types are among the most influential theories for verifying the absence of concurrency bugs in communicating systems. Session types can guarantee that process implementations only follow the specified structured sequence of actions (send/receive). These specifications effectively represent communication protocols, and session type theories provide techniques to verify that they are absent of concurrency bugs. Among the most influential extensions of session types is the theory of Multiparty Session Types (MPST), which enables the modelling of protocols among an arbitrary number of participants, and has been integrated with many mainstream languages.However, most of the tools based on session types are not following the exact theories that are presented in the scientific publications, since they also need to take into account engineering issues. Furthermore, most of the session type theories are proven correct using complex pen-and-paper soundness proofs. Such proofs can contain errors, and the literature shows examples of these cases. This is a big threat to the validity of large bodies of work. Proof assistants are tools that can guarantee the correctness of these soundness arguments. Encoding languages, tools, and theories in a proof assistant is called mechanisation, and it has led to large influential developments in computer science, such as CompCert, a certified C compiler that has proven to present significantly less bugs than other comparable compilers, and that is currently being used in the context of critical systems.But proof mechanisation is significantly hard, and not much work exists on mechanising MPST. One of the main hurdles in mechanising MPST is the notion of process equivalence, or bisimilarity. Informally, two processes are bisimilar if they match each others actions, according to their Labelled-state Transition System (LTS) semantics. One main techniques for proving bisimilarity is known as the bisimulation proof method, which relies on finding a relation between two processes that guarantees that they will match each other's moves according to their LTS. These proofs are widespread in concurrency theory, and are key to successful mechanisations of MPST. We need a way to simplify the mechanisation of LTS semantics, and bisimilarity proofs.We will study common bisimulation proof techniques and algorithms, and find and implement a suitable candidate for mechanisation. Our main goal is to automate as much as possible of the mechanisation of the LTS semantics. One of the key challenges is to find the suitable definitions: pen-and-paper proofs can often overlook details that are important in a mechanisation. For example, termination is often informally justified in pen-and-paper proofs, but the specific details are key to a successful mechanisation. We will mechanise a generic framework for LTS semantics and bisimilarity in the Coq proof assistant, and use it in two case studies from the project partners. These case studies will serve both as a way to evaluate success, and as main driving elements of this project. Finally, we will study the extraction of certified implementations within our framework, thus contributing to increase the safety and reliability of distributed systems.

构建正确的通信系统（即并发和分布式系统）是一项艰巨的任务。这样的系统通常呈现出难以再现的非确定性行为。这意味着，无论何时在这样的系统中出现错误，修复它都是一项耗时且昂贵的任务。此外，分布式系统如今在我们的社会中广泛存在，包括银行或电子医疗等关键部门。因此，通信系统中的错误可能是非常具有破坏性的，威胁到巨大的经济成本，以及依赖于它们的行业的安全性。会话类型是验证通信系统中不存在并发错误的最有影响力的理论之一。会话类型可以保证流程实现只遵循指定的结构化操作序列（发送/接收）。这些规范有效地表示了通信协议，会话类型理论提供了验证它们不存在并发错误的技术。其中最有影响力的会话类型的扩展是多方会话类型（MPST）的理论，它允许在任意数量的参与者之间建模协议，并已与许多主流语言集成。然而，大多数基于会话类型的工具并不遵循科学出版物中提出的确切理论，因为它们还需要考虑工程问题。此外，大多数会话类型理论都是使用复杂的笔和纸的可靠性证明来证明的。这样的证明可能包含错误，文献显示了这些情况的例子。这是对大量工作有效性的巨大威胁。证明助手是可以保证这些可靠性参数正确性的工具。将语言、工具和理论编码在证明助手中被称为机械化，它在计算机科学中产生了巨大的影响力，例如CompCert，一个经过认证的C编译器，它被证明比其他类似的编译器存在更少的错误，目前正在关键系统的上下文中使用。但是证明机械化非常困难，并且没有太多的工作存在于机械化MPST。MPST机械化的主要障碍之一是过程等价或双相似性的概念。非正式地，两个进程是双向相似的，如果他们匹配对方的行动，根据他们的标签状态转换系统（LTS）的语义。证明双相似性的一个主要技术被称为互模拟证明方法，它依赖于找到两个进程之间的关系，保证它们将根据LTS匹配彼此的移动。这些证明在并发理论中很普遍，并且是MPST成功机制的关键。我们需要一种方法来简化LTS语义的机械化，以及双相似性证明。我们将研究常见的互模拟证明技术和算法，并找到和实现一个合适的机械化候选者。我们的主要目标是尽可能多地自动化LTS语义的机械化。关键的挑战之一是找到合适的定义：纸笔证明往往会忽略机械化中重要的细节。例如，终止通常在纸笔证明中被非正式地证明是合理的，但具体的细节是成功的机械化的关键。我们将在Coq证明助手中机械化LTS语义和双相似性的通用框架，并将其用于项目合作伙伴的两个案例研究中。这些案例研究将作为评估成功的一种方式，并作为该项目的主要驱动因素。最后，我们将研究在我们的框架内提取认证的实现，从而有助于提高分布式系统的安全性和可靠性。