Pi - Calculus Research And Implementation Of Interactive Verification Tool

Concurrent systems play so important roles in many projects that their correctness should be carefully considered. How to ensure the correctness becomes an valuable task.Process algebras are widely used in describing and analyzing concurrent systems. Among them,the -calculus is the one capable of modelling concurrent systems with evolving communicating structures.When large system is under consideration,the proof process using the -calculus will be long and error-prone. Therefore,some kind of mechanical support is necessary. Our task is to develop the first interactive proof assistant for the -calculus. We call it PiM(the Pi-calculus Manipulator). Our work includes the following three aspects.First,aiming at designing a suitable version of the unique fixpoint induction from the application point of view,we generalized Lin's version and got the final version we needed.Second,we implemented PiM,the first interactive proof assistant for the -calculus. PiM bases on the proof systems for the late and early bisimulation congruences and the open bisim-ulation congruences. We implemented our version of the unique fixpoint induction to deal with recursions.At last,we proved the AB protocol (the Alternation Bit protocol) in PiM. In doing so,we found an error concerning the AB protocol in R. Milner's book "Communication and Concurrency" .The results about the unique fixpoint induction are of theoretical significance. The proof assistant PiM is of importance from the application point of view. Moreover,the verification of the AB protocol and the discovery of an error in R. Milner's book point out the value of our work.