Formalizing Process Algebraic Verifications in the Calculus of Constructions

摘要

This paper reports on the first steps towards the formal verification ofcorrectness proofs of real-life protocols in process algebra. They show that proofs can be verified, and partly constructed, by a general purpose proof checker. The process algebra the authors use is muCRL, ACP(sup r) augmented with data, which is small enough to make the verification feasible, and at the same time expressive enough for the specification of real-life protocols. The proof checker the authors use is Coq, which is based on the Calculus of Constructions, an extension of simply typed lambda calculus. The focus is on the translation of the proof theory of muCRL and muCRL-specifications to Coq. As a case study, the authors verified the Alternating Bit Protocol.