Cones and foci: A mechanical framework for protocol verification |
| |
Authors: | Wan Fokkink Jun Pang Jaco van de Pol |
| |
Affiliation: | (1) CWI, Specification and Analysis of Embedded Systems Group, Kruislaan 413, 1098 SJ Amsterdam, The Netherlands;(2) Vrije Universiteit, Section of Theoretical Computer Science, 1081 HV, Amsterdam, The Netherlands;(3) INRIA Futurs and LIX, école Polytechnique, F-91128 Palaiseau Cedex, France;(4) Eindhoven University of Technology, Design and Analysis of Systems Group, 5600 MB Eindhoven, The Netherlands |
| |
Abstract: | We define a cones and foci proof method, which rephrases the question whether two system specifications are branching bisimilar in terms of proof obligations on relations between data objects. Compared to the original cones and foci method from Groote and Springintveld, our method is more generally applicable, because it does not require a preprocessing step to eliminate τ-loops. We prove soundness of our approach and present a set of rules to prove the reachability of focus points. Our method has been formalized and proved correct using PVS. Thus we have established a framework for mechanical protocol verification. We apply this framework to the Concurrent Alternating Bit Protocol.
|
| |
Keywords: | Protocol verification Branching bisimulation Process algebra PVS |
本文献已被 SpringerLink 等数据库收录! |
|