Toward Proving the Correctness of TCP Protocol Using CTL
Journal: The International Arab Journal of Information Technology (Vol.16, No. 3)Publication Date: 2019-05-01
Authors : Rafat Alshorman;
Page : 407-414
Keywords : CTL; model checking; TCP protocols; correctness conditions; kripkestructure.;
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 formulaeComputational Tree Logic (CTL). Then, Model checker interprets these temporal formulae over the FSM to check whether the correctness conditions are satisfiedor not. Moreover, the introduced model of the protocol, in this paper, is modelling the concurrent synchronized clients and servers to be iterated infinite often.
Other Latest Articles
- A Dynamic Architecture forRuntimeAdaptation of Service-based Applications
- Contrast Enhancement using Completely Overlapped Uniformly Decrementing Sub-Block Histogram Equalization for Less Controlled IlluminationVariation
- Machine Translation Infrastructure for Turkic Languages (MT-Turk)
- PeSOA: Penguins Search Optimisation Algorithm for Global Optimisation Problems
- Preceding Document Clustering by Graph Mining Based Maximal Frequent Termsets Preservation
Last modified: 2019-04-28 20:01:36