Formal Verification of Arbitrary Network Topologies
Sadie Creese, Andrew William Roscoe · 1999
We show how data independence results can be used to generalise an inductive proof from binary to arbitrary branching tree networks. The example used is modelled on the RSVP Resource Reservation Protocol. Of particular interest is the need for a separate lower-level induction which is itself closely tied to data independence. The inductions combine the use of the process algebra CSP to model systems and their specifications, and the FDR tool to discharge the various proof obligations.