We present
a verification technique based on network symmetry classes along with
a manually derived abstraction that allows us to show, at the
bus/bridge level, that all execution traces of all acyclic PCI
networks satisfy the transaction ordering property. This now
completed case study suggests several avenues for further work in
combining model-checking (algorithmic methods) and theorem-proving
(deductive methods) in judicious ways to solve infinite-state
verification problems at the bus/interconnect level. It is a concrete
illustration of partitioning concerns where designers can specify bus
protocols in an operational semantics (rule-based) style, invent
abstractions, and carry out finite-state model-checking while
verification experts can establish formal properties of the
abstraction.
