Modeling a transport layer protocol using first-order logic

摘要

We use a hybrid model based on the first-order logic to specify and verify a transport layer protocol. In this model we specify a protocol as a set of state machines. Time expressions are used to describe the temporal relations of transitions. Given the specification of a protocol, we verify its properties by logical deduction. Reasoning techniques such as decomposition and abstraction are used to reduce the verification complexity.

rn

The transport protocol consists of an active process, a passive process, and two communication channels. Each of these components is specified by this model. An outline of verification of this protocol is given.