formal verification methods, parameterized systems, predicate abstraction
We have used various manual abstraction techniques to formally verify a transaction ordering property for an IO protocol over bus/bridge networks. In the context of network protocol verification, an abstraction is needed to reduce the unbounded number of network configurations to a small number of representative networks that can be checked using algorithmic methods. The manually derived abstraction was both brittle and difficult to validate. In this report, we discuss the need for abstraction techniques in the formal verification of protocols over networks and present our recent efforts to create an automatic abstraction technique for network protocols using predicate abstraction as a starting point.
Original Publication Citation
M. Jones and G. Gopalakrishnan, "Toward Automated Abstraction for Protocols Over Branching Networks," IEEE International High Level Design Validation and Test Workshop (HLDVT'), pp. 147-154. Palo Alto, California, November 2.
BYU ScholarsArchive Citation
Jones, Michael D. and Gopalakrishnan, Ganesh, "Toward Automated Abstraction for Protocols on Branching Networks" (2000). All Faculty Publications. 587.
Physical and Mathematical Sciences
© 2000 Institute of Electrical and Electronics Engineers
Copyright Use Information