Framework and Tool Support for Formal Verification of Highspeed Transfer Protocol Designs

Formal description techniques, verification methods, and their tool-based automated application meanwhile provide valuable support for the formal analysis of communication protocol designs. Nevertheless the practical analysis of modern protocols still requires relatively great efforts and therefore many protocol developments do not employ formal methods. In that context the transfer protocol framework aims to complementary support. It supplies a rich collection of specification modules and guides their efficient composition to service and protocol specifications. Moreover the functional relations between service properties and implementing protocol mechanisms have been investigated systematically. The framework provides a collection of corresponding theorems to be applied to protocol correctness proofs. In result protocol verification can be reduced to the selection, instantiation, and proper arrangement of framework theorems. The verification process can further be supported by specia...

• Type: Journal
• Year: 2002
• Where: TELSYS
• Authors: Peter Herrmann, Heiko Krumm, Olaf Drögehorn, Walter Geisselhardt
• Keywords: Framework Theorems, Protocol Specification, TELSYS 2002, Transfer Protocol Framework