We investigate a technique, suitable for process algebraic, finite-state machine automated tools, for formally modelling arbitray network topologes. We model aspects of a protocol for multiservice networks, and demonstrate how the technique can be sued to verify end-to-end properties of protocols designed for arbitrary number s 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.
展开▼
