Technical reports

Formalising process calculi in Higher Order Logic

Monica Nesi

January 1997, 182 pages

This technical report is based on a dissertation submitted April 1996 by the author for the degree of Doctor of Philosophy to the University of Cambridge, Girton College.

Abstract

In the past few years, several methods and tools based on process calculi have been developed for verifying properties of concurrent and communicating systems. In this dissertation the interactive theorem prover HOL is used as a framework for supporting reasoning about process calculi based on all the various components of their formal theory. The aim is to build a sound and effective tool to allow both verification of process specifications and meta-theoretic reasoning. In particular the process calculus CCS is embedded in HOL logic. This is achieved by first addressing the pure subset of this calculus (no value passing) and then extending it to its value-passing version. The CCS theory is mechanised in HOL by following a purely definitional approach. This means that new objects are embedded in HOL using definition mechanisms which guarantee that no inconsistencies are introduced in the logic, and by deriving new facts from definitions and/or previously proved theorems by formal proof.

Pure CCS agent expressions are encoded as a type in the HOL logic, in which initially actions are represented as strings, agents with infinite behaviour are given through the rec-notation and agent summation is the usual binary operator. Recursive agents are then allowed to be defined through systems of recursive equations and to be parameterised. This makes the type of CCS expressions polymorphic and parameterised on the parameters’ type. Operational and behavioural semantics and modal logic are defined and their properties and laws derived in HOL. Several proof tools, such as inference rules, conversions and tactics, are developed to enable users to carry out their proofs in an interactive way and to automate them whenever possible. Properties of infinite state systems, e.g. a counter which can expand indefinitely, can be formally verified in the resulting proof environment.

Then value-passing CCS is mechanised in HOL by translating value-passing expressions into pure ones. This entails a more general polymorphic type for pure agent expressions that includes an indexed summation operator. The translation is proved to be correct with respect to the semantics of value-passing CCS and then used at meta-level, together with the HOL formalisation for pure CCS, for developing behavioural theories for the value-passing calculus. A proof environment is thus derived, in which users will directly work on the value-passing specifications. A verification example illustrates how proofs about the data are neatly separated from proofs about the process behaviour and how ω-data-rules can be used in a practical way to reason about value-passing agents defined over an infinite value domain.

Full text

PDF (16.7 MB)

BibTeX record

@TechReport{UCAM-CL-TR-411,
  author =	 {Nesi, Monica},
  title = 	 {{Formalising process calculi in Higher Order Logic}},
  year = 	 1997,
  month = 	 jan,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-411.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-411},
  number = 	 {UCAM-CL-TR-411}
}