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.

References

[1] Adalid D., Salmeron A., Gallardo M., and Merino P., “Using SPIN for Automated Debugging of Infinite Executions of Java Programs,” Journal of Systems and Software, vol. 90, no. 5, pp. 61-75, 2014. 111()j i n j m jiiA G R oA F C      412 The International Arab Journal of Information Technology, Vol. 16, No. 3, May 2019

[2] Alshorman R. and Hussak W., “A CTL Specification of Serializability for Transactions Accessing Uniform Data,” International Journal of Computer Science and Engineering, vol. 3, no. 5, pp. 26-32, 2009.

[3] Casoni M., Grazia C., Klapez M., and Patriciello N., “Implementation and Validation of TCP Options and Congestion Control Algorithms for Ns-3,” in Proceedings of the Workshop on ns-3, Barcelona, pp.112-119. 2015.

[4] Cimatti A., Clarke E., Giunchiglia F., and Roveri M., “NuSMV: A New Symbolic model Verifier,” in Proceedings of the 11th International Conference on Computer Aided Verification, London, pp. 495-499, 1999.

[5] Comer D., Computer Networks and Internets, Pearson, 2014.

[6] Debiao H., Jianhua C., and Jin H., “An ID-Based Client Authentication with Key Agreement Protocol for Mobile Client-Server Environment on ECC with Provable Security,” Information Fusion, vol. 13, no. 3, pp. 223-230, 2010.

[7] Gnesi S., “Formal Specification and Verification of Complex Systems,” Electronic Notes in Theoretical Computer Science Netherlands, vol. 80, pp. 294-298, 2003.

[8] Gray D., Hamilton G., and Sinclair D., “Four Logics and a Protocol,” in Proceedings of the 3rd Irish Conference on Formal Methods, Swinton, pp. 79-102, 1999.

[9] He C., Sundararajan M., Datta A., Derek A., and Mitchell J., “A Modular Correctness Proof of IEEE 802.11i and TLS,” in Proceedings of the 12th ACM Conference on Computer and Communications Security, Alexandria, pp. 2-15. 2005.

[10] Hussak W., “Monodic Temporal Logic with Quantified Propositional Variables,” Journal of Logic and Computation, vol. 22, no. 3, pp. 517- 544, 2012.

[11] Hussak W., “Serializable Histories in Quantified Propositional Temporal Logic,” International Journal of Computer Mathematics, vol. 81, no. 10, pp. 1203-1211, 2004.

[12] Ibrahim S., Idris B., Munro M., and Deraman A., “Integrating Software Traceability For Change Impact Analysis,” The International Arab Journal of Information Technology, vol. 2, no. 4, pp. 301-308, 2005.

[13] Kerber M., Lange C., and Rowat C., “An Introduction to Mechanized Reasoning,” Journal of Mathematical Economics, vol. 66, pp. 26-39, 2016.

[14] Pucella R., “The Finite and the Infinite in Temporal Logic,” ACM SIGACT, vol. 36, no. 1, pp. 86-99, 2005.

[15] Ran G., Zhang H., and Gong S., “Improving on LEACH Protocol of Wireless Sensor Networks Using Fuzzy Logic,” Journal of Information and Computational Science, vol. 7, no. 2, pp. 767- 775, 2010.

[16] Salmeron A. and Merino P., “Integrating Model Checking and simulation for Protocol Optimization,” Simulation: Transactions of the Society for Modeling and Simulation International, vol. 91, no. 1, pp. 3-25, 2015.

[17] Shatnawi m., “Discrete Time NHPP Models for Software Reliability Growth Phenomenon,” The International Arab Journal of Information Technology, vol. 6, no. 2, pp. 124-131, 2009. Rafat Alshorman is an assistant professor in the department of computer science at Yarmouk University/Jordan. Dr. Alshorman completed his Ph.D. at Loughborough University/UK and his under graduate studies at Yarmouk University/Jordan. His research interests lie in the area of algorithms and mathematical models, ranging from theory to implementation, with a focus on checking the correctness conditions of concurrent and reactive systems. In recent years, he has focused on theoretical computer science such as Graph theory and Numerical analysis. Dr. Alshorman research interests are: 1. Mathematical methods in computer science 2. Temporal logics 3. Concurrent systems 4.Serializability of Transactions 5.Numerical analysis. Toward Proving the Correctness of TCP Protocol Using CTL 413 Appendix A --------------------------------------------------- MODULE client(qs1,qs2,st) --------------------------------------------------- VAR process_c:{p1,p2}; state: {idle, req, rej, wait, rec, comp}; --------------------------------------------------- ASSIGN init(process_c) :={p1,p2}; init(state) := idle; next(state) :=case state=idle & process_c=p1 & qs1!=2: req; state=req & process_c=p1 & qs1!=2: wait; state=req & process_c=p1 & qs1=2: rej; --no space in socket 1 state=wait & process_c=p1 &st!=busy: rec; state=rec : comp; state=rej : req; --request again state=comp :idle; --iterate infinitely often state=idle & process_c=p2 & qs2!=2: req; state=req & process_c=p2 & qs2!=2: wait; state=req & process_c=p2 & qs2=2: rej; --no space in socket 2 state=wait &process_c=p2 &st!=busy: rec; TRUE : state; esac; --------------------------------------------------- next(process_c) :=case process_c=p1 & state!=comp : p1; process_c=p1 & state=comp : {p1,p2}; process_c=p2 & state!=comp : p2; process_c=p2 & state=comp : {p1,p2}; TRUE : process_c; esac; --------------------------------------------------- MODULE server (queuesoc1,queuesoc2) --------------------------------------------------- VAR state_s :{idle, pro, busy}; --------------------------------------------------- ASSIGN init(state_s):=idle; next(state_s) :=case state_s=idle & queuesoc1 =-1 & queuesoc2 =-1 : idle; state_s=idle & queuesoc1!=2 & queuesoc1!=2 : pro; state_s=pro & queuesoc1=2 & queuesoc1=2 : busy; TRUE: state_s; esac; --------------------------------------------------- MODULE Queue1 (st1,pr1,st2,pr2,st3,pr3) --------------------------------------------------- VAR queuesoc1 : -1..2; --------------------------------------------------- ASSIGN init (queuesoc1) := -1; next(queuesoc1) :=case queuesoc1=-1 & ((st1=req& pr1=p1)|(st2=req& pr2=p1)|(st3=req& pr3=p1)) : 0; queuesoc1=0 & ((st1=req& pr1=p1)|(st2=req& pr2=p1)|(st3=req& pr3=p1)) : 1; queuesoc1=1 & ((st1=req& pr1=p1)|(st2=req& pr2=p1)|(st3=req& pr3=p1)) : 2; queuesoc1=2 & ((st1=req& pr1=p1)|(st2=req& pr2=p1)|(st3=req& pr3=p1)): queuesoc1; queuesoc1=0 & ((st1=comp & pr1=p1)|(st2=comp & pr2=p1)|(st3=comp & pr3=p1)) : -1; queuesoc1=1 & ((st1=comp & pr1=p1)|(st2=comp & pr2=p1)|(st3=comp & pr3=p1)) : 0; queuesoc1=2 & ((st1=comp & pr1=p1)|(st2=comp & pr2=p1)|(st3=comp & pr3=p1)) : 1; queuesoc1=-1 & ((st1=comp & pr1=p1)|(st2=comp & pr2=p1)|(st3=comp & pr3=p1)): queuesoc1; TRUE: queuesoc1; esac; --------------------------------------------------- MODULE Queue2 (st1,pr1,st2,pr2,st3,pr3) --------------------------------------------------- VAR queuesoc2 : -1..2; --------------------------------------------------- ASSIGN init (queuesoc2):= -1; next(queuesoc2) :=case queuesoc2=-1 & ((st1=req& pr1=p2)|(st2=req& pr2=p2)|(st3=req& pr3=p2)) : 0; queuesoc2=0 & ((st1=req& pr1=p2)|(st2=req& pr2=p2)|(st3=req& pr3=p2)) : 1; queuesoc2=1 & ((st1=req& pr1=p2)|(st2=req& pr2=p2)|(st3=req& pr3=p2)) : 2; queuesoc2=2 & ((st1=req& pr1=p2)|(st2=req& pr2=p2)|(st3=req& pr3=p2)) : queuesoc2; queuesoc2=0 & ((st1=comp & pr1=p2)|(st2=comp & pr2=p2)|(st3=comp & pr3=p2)) : -1; queuesoc2=1 & ((st1=comp & pr1=p2)|(st2=comp & pr2=p2)|(st3=comp & pr3=p2)) : 0; 414 The International Arab Journal of Information Technology, Vol. 16, No. 3, May 2019 queuesoc2=2 & ((st1=comp & pr1=p2)|(st2=comp & pr2=p2)|(st3=comp & pr3=p2)) : 1; queuesoc2=-1 & ((st1=comp & pr1=p2)|(st2=comp & pr2=p2)|(st3=comp & pr3=p2)) : queuesoc2; TRUE: queuesoc2; esac; --------------------------------------------------- MODULE main --------------------------------------------------- VAR --------------------------------------------------- s:server(qu1.queuesoc1,qu2.queuesoc2); c1: client(qu1.queuesoc1,qu2.queuesoc2,s.state_s ); c2 : client(qu1.queuesoc1,qu2.queuesoc2,s.state_s ); c3 : client(qu1.queuesoc1,qu2.queuesoc2,s.state_s ); qu1: Queue1(c1.state,c1.process_c,c2.state,c2.process_c,c3. state,c3.process_c); qu2: Queue2(c1.state,c1.process_c,c2.state,c2.process_c,c3. state,c3.process_c); -------------------------------------------------------------- -------------SPECIFICATIONS------------------------- -------------------------------------------------------------- --Condition number 1 SPEC AG(c1.state=req ->AF c1.state=comp) SPEC AG(c2.state=req ->AF c2.state=comp) SPEC AG(c3.state=req ->AF c3.state=comp) LTLSPEC G(c1.state=req ->F c1.state=comp) LTLSPEC G(c2.state=req ->F c2.state=comp) LTLSPEC G(c3.state=req ->F c3.state=comp) -- Condition number 5 SPEC AG AF!(s.state_s=busy) --Condition number 6 SPEC AG((c1.state=rej& c1.process_c=p1) ->AF c1.state=comp) SPEC AG((c1.state=rej& c1.process_c=p2) ->AF c1.state=comp) SPEC AG((c2.state=rej& c2.process_c=p1) ->AF c2.state=comp) SPEC AG((c2.state=rej& c2.process_c=p2) ->AF c2.state=comp) SPEC AG((c3.state=rej& c3.process_c=p1) ->AF c3.state=comp) SPEC AG((c3.state=rej& c3.process_c=p2) ->AF c3.state=comp) -- Condition number 4 SPEC AG!(c1.state=rej& c1.process_c=p1 & qu1.queuesoc1!=2) SPEC AG!(c1.state=rej& c1.process_c=p2 & qu2.queuesoc2!=2) SPEC AG!(c2.state=rej& c2.process_c=p1 & qu1.queuesoc1!=2) SPEC AG!(c2.state=rej& c2.process_c=p2 & qu2.queuesoc2!=2) SPEC AG!(c3.state=rej& c3.process_c=p1 & qu1.queuesoc1!=2) SPEC AG!(c3.state=rej& c3.process_c=p2 & qu2.queuesoc2!=2) -- Condition number 2 SPEC AG ((c1.state=req -> AF c1.state=comp) & (c1.state=comp -> AF c1.state=req)) SPEC AG ((c2.state=req-> AF c2.state=comp) & (c2.state=comp -> AF c2.state=req)) SPEC AG ((c3.state=req-> AF c3.state=comp) & (c3.state=comp -> AF c3.state=req)) --Condition number3 SPEC AG ((qu1.queuesoc1=-1 & (c1.state=req& c1.process_c=p1))-> AX (qu1.queuesoc1=0)) SPEC AG ((qu1.queuesoc1=0 & (c1.state=req& c1.process_c=p1))-> AX (qu1.queuesoc1=1)) SPEC AG ((qu1.queuesoc1=1 & (c1.state=req& c1.process_c=p1))-> AX (qu1.queuesoc1=2)) SPEC AG ((qu2.queuesoc2=-1 & (c1.state=req& c1.process_c=p2))-> AX (qu2.queuesoc2=0)) SPEC AG ((qu2.queuesoc2=0 & (c1.state=req& c1.process_c=p2))-> AX (qu2.queuesoc2=1)) SPEC AG ((qu2.queuesoc2=1 & (c1.state=req& c1.process_c=p2))-> AX (qu2.queuesoc2=2)) -- condition that is produced counterexample(false) SPEC AG (qu1.queuesoc1=-1-> AX qu1.queuesoc1= -1)