Toward Proving the Correctness of TCP
Protocol Using CTL
Rafat Alshorman
Department of Computer Science, Yarmouk University, Jordan
Abstract:
The use of the Internet
requires two types of application programs. One is running in the first
endpoint of the network connection and requesting services, via application
programs, is called the client. The other, that provides the services, is
called the server. These application programs that are in client and server
communicate with each other under some system rules to exchange the services.
In this research, we shall try to model the system rules of communications that
are called protocol using model checker. The model checker represents the
states of the clients, servers and system rules (protocol) as a Finite State Machine
(FSM). The correctness conditions of the protocol are encoded into temporal
logics formulae Computational Tree Logic (CTL). Then, Model checker interprets
these temporal formulae over the FSM to check whether the correctness
conditions are satisfied or not. Moreover, the introduced model of the protocol,
in this paper, is modelling the concurrent synchronized clients and servers to
be iterated infinite often.
Keywords: CTL, model checking, TCP protocols, correctness
conditions, kripke structure.