A Framework for Modeling Transfer Protocols
Universität Dortmund, FB Informatik, LS IV, D-44221 Dortmund, Germany
The notion of specification frameworks transposes the framework approach from software development to the
level of formal modeling and analysis. A specification framework is devoted to a special application domain.
It supplies re-usable specification modules and guides the construction of specifications. Moreover, it
provides theorems to be used as building blocks of verifications. By means of a suitable framework,
specification and verification tasks can be reduced to the selection, parametrization and combination of
framework elements resulting in a substantial support which opens formal analysis even for real-sized
problems. The transfer protocol framework addressed here is devoted to the design of data transfer
protocols. Specifications of used and provided communication services as well as protocol specifications can
be composed from its specification modules. The theorems correspond to the relations between protocol
mechanism combinations and those properties of the provided service which are implemented by them. This
article centers on the application of this framework which is discussed with the help of the specification
of a sliding window protocol. Moreover the structure of its verification is described. The specification and
verification technique applied is based on L. Lamport's Temporal Logic of Actions (TLA). We use the variant
cTLA which particularly supports the modeling of process systems.
Protocol specification, Protocol verification,
Temporal logic, Framework, Protocol composition
Computer Networks, 34(2000)2, 317-337, Elsevier Science.
Obtaining the paper
Due to the copyright agreement between the publisher and the authors we are
not allowed to make the paper available online. If you have problems to
please call us.
Peter Herrmann, August 3, 2000
-- digital media copyright