Automated Protocol Verification.
UNIVERSITY OF SOUTHERN CALIFORNIA MARINA DEL REY INFORMATION SCIENCES INST
Pagination or Media Count:
Four general-purpose automated verification systems Affirm, Formal Development Methodology Ina Jo, Gypsy, and Concurrent State Deltas were applied to computer network protocols in order to evaluate the ability of such systems to provide significant results in formal protocol specification and verification. Each system had a particular strength Affirm was most polished and flexible FDM supported abstract machine specifications directly Gypsy supported stateless IO InputOutput history type specifications CSD supported more automatic proof and timing properties. However, none of the systems had all necessary features or was powerful enough to fully handle complex protocols. The relative strengths of the systems are compared, detailed examples of their use are presented, and suggestions for further work are given. Author
- Computer Programming and Software
- Computer Hardware
- Computer Systems