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 special tool-assistance. The tool COAST identifies the compositional structure of a protocol specification mechanically and selects according framework theorems. It splits service property proofs into arrangements of subproofs where the subproofs can mainly be accomplished by application of the selected framework theorems. After outlining the general transfer protocol framework approach we concentrate on the introduction of the tool COAST. We describe its functions and clarify its application by means of the verification of the complex real-life high-speed data transfer protocol XTP.