Formalising Process Composition for Complex Domains

形式化复杂领域的流程组合

• 批准号: 2425191
• 金额: --
• 依托单位: University of Edinburgh
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2020
• 资助国家: 英国
• 起止时间: 2020 至 无数据
• 项目状态: 已结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2425191
• 关键词: Formalising; Process; Composition; Complex; Domains

The world is full of concurrent processes. In the physical world there are machines in factories working together in complicated workflows, as well as people each doing their own work. In the virtual world, systems from cloud servers to mobile phones rely on concurrency. To better understand these systems, we have modelling languages like Petri nets or process calculi. However, these representations of real systems quickly get too large for humans to efficiently manipulate.The main objective of this project is to mechanise a formal theory of correct-by-construction process composition. We will mechanise this theory in the interactive theorem prover Isabelle/HOL, resulting in machine-checked proofs and lending further confidence to the correctness of our results. To demonstrate the usability of the theory, we will then formally verify a system of operations to assist humans in working with complex formal representations of workflows while ensuring correctness is preserved throughout the process. On top of this system, we can build tools to allow domain experts to compose simple processes into representations of complex real-life workflows. Because the resulting representation is fully formal, it can be further analysed and understood by automated tools allowing for example performance modelling or bottleneck detection. Because the operations are formally verified, we can be confident that the resulting representation for example correctly accounts for all inputs and outputs, and introduces no deadlock.This kind of modelling can be used in healthcare to model patient pathways, in manufacturing for shop floor scheduling and improving performance, or in administration to check conformance. With a mechanised representation of these processes, computers can be made to better understand them and aid in tasks that are now mainly done by humans. This in turn makes it possible to do things that are intractable for humans, especially when working with large numbers of concurrent processes, such as quick rescheduling in response to changing circumstances or priorities.We will use linear logic to express process specifications and compositions, using the proofs as processes paradigm to relate linear logic proofs to process calculus agents. The process representation will be an instance of psi-calculi, which are a framework for process calculi based on pi-calculus. This framework allows for structured data terms, which will let us tie the composition logic and the process representation closer together. It also has the capabilities of a number of extensions of pi-calculus, extending the range of processes we can express compared to just pi-calculus. Finally, the theory of psi-calculi is already mechanised in Isabelle/HOL which saves a substantial amount of work.We will also consider various useful extensions to this core idea, for instance the following four. First, extending the composition logic beyond simple propositions would allow us to express finer details in the process specifications. With those we could derive stronger guarantees about the results of composition. Second, psi-calculi have a higher-order extension which allows us to express, among other things, recursive processes. If we find a natural way of expressing these in the composition logic, we would then be able to describe another range of processes. Third, because psi-calculi are based on the pi-calculus which has a stochastic extension, we should be able to find such an extension for our process representation as well. This would let us extract Continuous Time Markov Chain models of the processes, which can then be used to model their performance in standard ways. Fourth, because linear logic forms a symmetric monoidal category, category theory might bring some insights to our view on process composition. It provides another perspective on the structures we encounter, pointing out parallels with other areas of mathematics potentially with useful lessons.

这个世界充满了并发的过程。在物理世界中，工厂中的机器在复杂的工作流程中一起工作，以及每个人都在做自己的工作。在虚拟世界中，从云服务器到移动的电话的系统都依赖于并发性。为了更好地理解这些系统，我们有建模语言，如Petri网或进程演算。然而，这些表示的真实的系统很快就变得太大，人类有效地manipulation.The主要目标是机械化的一个正式的理论正确的建设过程组成。我们将在交互式定理证明器Isabelle/HOL中机械化这一理论，从而产生机器检查的证明，并进一步增强对我们结果正确性的信心。为了证明该理论的可用性，我们将正式验证操作系统，以帮助人类处理工作流的复杂正式表示，同时确保在整个过程中保持正确性。在这个系统之上，我们可以构建工具，允许领域专家将简单的流程组合成复杂的现实工作流的表示。由于所得到的表示是完全形式化的，因此可以通过自动化工具进一步分析和理解，例如性能建模或瓶颈检测。由于操作经过了形式化验证，因此我们可以确信最终的表示正确地解释了所有输入和输出，并且不会引入死锁。这种建模可以用于医疗保健中对患者路径进行建模，用于制造车间调度和提高性能，或用于管理中检查一致性。通过对这些过程的机械化表示，计算机可以更好地理解它们，并帮助完成现在主要由人类完成的任务。这反过来又使得人们可以做一些难以处理的事情，特别是当处理大量并发进程时，例如快速重新调度以响应不断变化的环境或优先级。我们将使用线性逻辑来表达流程规范和组合，使用证明作为流程范例来将线性逻辑证明与流程演算代理相关联。进程表示将是psi-calculi的一个实例，psi-calculi是一个基于pi演算的进程演算框架。这个框架允许使用结构化数据术语，这将使我们能够将组合逻辑和流程表示更紧密地联系在一起。它还具有许多pi演算扩展的功能，与pi演算相比，扩展了我们可以表达的过程的范围。最后，PSI演算理论已经在Isabelle/HOL中实现了机械化，这节省了大量的工作。我们还将考虑对这个核心思想的各种有用的扩展，例如以下四个。首先，将组合逻辑扩展到简单的命题之外将允许我们在过程规范中表达更精细的细节。有了这些，我们就可以得到关于合成结果的更强有力的保证。其次，PSI演算有一个高阶扩展，它允许我们表达递归过程等。如果我们在组合逻辑中找到一种自然的方式来表达这些，那么我们就能够描述另一系列的过程。第三，因为PSI演算是基于具有随机扩展的Pi演算，所以我们也应该能够为我们的过程表示找到这样的扩展。这将使我们能够提取过程的连续时间马尔可夫链模型，然后可以使用这些模型以标准方式对其性能进行建模。第四，因为线性逻辑形成了一个对称的monoidal范畴，范畴论可能会给我们关于过程组成的观点带来一些启示。它提供了另一个视角，我们遇到的结构，指出与其他领域的数学潜在的有用的教训的相似之处。