Formalising Process Composition for 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.