首页 | 本学科首页   官方微博 | 高级检索  
     


Formalizing process algebraic verifications in the calculus of constructions
Authors:Marc Bezem  Roland Bol  Jan Friso Groote
Affiliation:(1) Dept. of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, The Netherlands;(2) Dept. of Computing Science, Uppsala University, Uppsala, Sweden;(3) Dept. of Software Technology, CWI, Amsterdam, The Netherlands
Abstract:This paper reports on the first steps towards the formal verification of correctness proofs of real-life protocols in process algebra. We show that such proofs can be verified, and partly constructed, by a general purpose proof checker. The process algebra we use ismgrCRL, ACPtau augmented with data, which is expressive enough for the specification of real-life protocols. The proof checker we 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 ofmgrCRL andmgrCRL-specifications to Coq. As a case study, we verified the Alternating Bit Protocol.
Keywords:Formal verification  Process algebra  ACP  gmCRL  Coq  Calculus of Constructions  Alternating Bit Protocol
本文献已被 SpringerLink 等数据库收录!
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号