Paper Details

Working Towards the Agreement Problem Protocol Verification Environment

Authors: Pascoe, James S., Loader, Roger J., Sunderam, Vaidy S.

Abstract:

This paper proposes the Agreement Problem Protocol Verification Environment (APPROVE) for the automated formal verification of novel solutions to agreement problems in group communication systems. Agreement problems are characterized by the need for a group of processes to agree on a proposed value and are exemplified by group membership, consensus and fault-tolerance scenarios. Due to their fundamental role, it is important that the correctness of new agreement algorithms be verified formally. In the past, the application of manual proof methods has been met with varying degrees of success, suggesting the need for a less error prone automated approach. An observation concerning previous proofs is that often a significant amount of effort is invested in modeling themes common to all such proofs, albeit using different formalisms. Thus, the APPROVE project aims to address these issues, its envisaged culmination being a usable software framework that exploits model re-use wherever possible.

Proceedings:

Communicating Process Architectures 2001, Alan G. Chalmers, Majid Mirmehdi, Henk Muller, 2001, pp 213 - 230 published by IOS Press, Amsterdam

This record in other formats: