Computing at Glasgow University
Paper ID: 8203
DCS Tech Report Number: TR-2006-220

Verifying parameterised networks by abstraction and induction: experience from the IEEE 1394 protocol
Miller,A. Calder,M.

Publication Type: Tech Report (internal)
Appeared in: DCS Technical Report Series
Page Numbers : 39
Publisher: Dept of Computing Science, University of Glasgow
Year: 2006

We present two techniques for reasoning about the behaviour of arbitrary-sized networks of concurrent, communicating processes, and apply them to the IEEE 1394 tree identity protocol. The first technique involves the construction of a network invariant and combines data and behavioural abstraction with model checking to generalise indexed safety properties and existential liveness properties for networks with a star topology of any size. We show how this approach can be extended to systems whose topology belongs to any of a set of families (of acyclic topologies). The second technique is a lightweight induction approach in which we exploit the degenerative nature of the protocol. This novel approach uses induction to generalise unindexed liveness properties for all acyclic networks of any size.

Keywords: firewire, verification, induction

PS/PS.GZ PDF Bibtex entry Endnote XML