Verifying end-to-end protocols using induction with CSP/FDR

Abstract

We investigate a technique, suitable for process algebraic, finite-state machine (model-checking) automated tools, for formally modelling arbitrary network topologies. We model aspects of a protocol for multiservice networks, and demonstrate how the technique can be used to verify end-to-end properties of protocols designed for arbitrary numbers of intermediate nodes. Our models are presented in a version of CSP allowing automatic verification with the FDR software tool. They encompass both inductive and non-inductive behaviours.