|
Abstract : |
Abstract We extend the classes of network which Data Independent Induction can be used to reason about. Through the use of constants and predicates in the data independent type we build proofs of structured networks ' behaviours, where a network's topology need not be as regular as one might expect data independence to imply. These properties hold true independent of the size of the type, and so for arbitrary network size. The inductions combine the use of the process algebra CSP to model systems and their specications, and the FDR tool to discharge the various proof obligations. Keywords: induction, data independence, CSP, FDR, model-checking. 1, |
