Formal verification of parameterized protocols on branching networks

Verifying the functional correctness of a parameterized protocol on all valid branching networks is a difficult problem that can not be solved using simulation alone because the number and shape of valid branching networks is unbounded. This problem is of particular interest because multibus IO and memory protocols can be modelled as parameterized protocols on branching networks.; The central result of the thesis is a model checking algorithm for verifying functional correctness properties of a protocol on a family of topologically which over-approximate the reachable states for the protocol. Concrete transitions The algorithm is supported by a specification language, topological case split and generalization argument.; The algorithm, specification language and case split have been implemented in the Πcasso model checker. Πcasso has been used to verify the producer/consumer transaction ordering property for a corrected version PCI 2.1 multibus networks. Πcasso has also been used to find a configuration dependent violation of a write coherence property in PCI networks. Since PCI was not intended to satisfy this property, the significance of this violation is not that it is present in one class of configurations, but that it is not present in every other class of configurations.