MODULAR SPECIFICATION AND VERIFICATION OF XTP

The transfer protocol framework supports the formal specification and verification of data transfer protocols. It consists of generic specif ication modules and theorems. Compositions of specification module ins tances result in well-structured specifications which describe a proto col, the medium used, and the service provided by means of TLA formula s. The protocol verification is based on the proof of the logical impl ication between protocol and service specification. Due to the modular structuring of the specifications, this proof can be decomposed into a set of subimplications which correspond directly to theorems of the framework. Therefore, the development of formal specifications as well as the protocol verification can be reduced to the instantiation and arrangement of framework elements. The flexibility of the framework op ens its application for a broad spectrum of data transfer protocols. W e outline the principles of the framework and concentrate on its appli cation to the high-speed transfer protocol XTP. Because of the framewo rk support, the formal modeling and analysis of this modem and functio n-rich protocol was manageable and identifies deficiencies of the curr ent protocol definition clearly.