Keywords: process algebra, Isabelle/HOL, proof mechanisation
Units: 24 units
Background
The milli Common Representation Language (mCRL2) [GM14] is a formal specification language (process algebra) with an associated collection of tools offering support for model checking, simulation, state-space generation, as well as for the optimisation and analysis of specifications [CGKSVWW13]. The toolset has been used in countless case studies, including the analysis software for the CERN’s Large Hadron Collider, and the IEEE 1394 link layer [Lut97].
While the set of tools for mCRL2 is impressive, the tools fail short when it comes to proof mechanisation. By proof mechanisation we mean support by interactive proof assistants, such as Isabelle/HOL [NPW02].
Mechanising process calculi and process-algebraic models in proof assistants can almost be considered routine. However, a lot of this work focuses on process calculi themselves; little work has been done on mechanising the application of such calculi to the practical verification of network protocols.
Research Questions and Tasks
The aim of this research project is to develop a framework for the process algebra mCRL2 in Isabelle/HOL. This will include the following tasks.
- Extend the existing mechanisation of the process algebra ACP (a sublanguage of mCRL2) to cover all aspects of the untimed version of mCRL2; in particular this includes the integration of data structures into the framework.
- Develop a framework for the complete syntax and semantics of mCRL2, including aspects of time.
- (for 24 credits) The developed theory should be used to mechanise (and automate) an existing (constructive) proof of a theorem that states that any process written in AWN (yet another process algebra) can be encoded in mCRL2.
The development should follow modern techniques and guidelines for Isabelle/HOL, e.g. [NK14] Ideally, the project will be submitted to the Archive of Formal Proofs(https://www.isa-afp.org) after successful completion.
References
- [CGKSVWW13] S. Cranen, J.F. Groote, J.J.A. Keiren, F.P.M. Stappers, E.P. de Vink, W. Wesselink & T.A.C. Willemse(2013): An Overview of the mCRL2 Toolset and Its Recent Advances. In N. Piterman & S. Smolka, editors: TACAS’13, LNCS 7795, Springer, pp. 199–213, doi:10.1007/978-3-642-36742-7_15.
- [GM14] J.F. Groote & M.R. Mousavi (2014): Modeling and analysis of communicating systems. MIT Press.
- [Lut97] S.P. Luttik (1997): Description and Formal Specification of the Link Layer of P1394. In I. Lovrek, editor: 2nd International Workshop on Applied Formal Methods in System Design, pp. 43–56.
- [NK14] T. Nipkow & G. Klein (2014): Concrete Semantics: With Isabelle/HOL. Springer, doi:10.1007/978-3-319-10542-0.
- [NPW02] T. Nipkow, L.C. Paulson & M. Wenzel (2002): Isabelle/HOL \ndash; A Proof Assistant for Higher-Order Logic. LNCS 2283, Springer, doi: 10.1007/3-540-45949-9.
Requirements: Process algebra, some experience with interactive theorem provers such as Isabelle/HOL, Coq or HOL is of advantage.