To search, Click below search items.


All Published Papers Search Service


Modeling and Formal Verification of Communication Protocols for Remote Procedure Call


Nilimesh Halder, A.B.M Tariqul Islam, Ju Bin Song


Vol. 7  No. 7  pp. 63-71


This paper presents the modeling and formal verification of some communication protocols for Remote Procedure Call (RPC). These protocols include Request (R) Protocol, Request Reply (RR) Protocol and Request-Reply-Acknowledgement (RRA) Protocol. We have modeled the above-mentioned protocols in Symbolic Model Verifier (SMV), a formal verification tool. In modeling of each protocol, each of the two agents (Client and Server) is modeled as a finite state machine. The common channel between these agents is modeled as a bounded queue of message. Some important features of modeled protocols are then formal verified using the SMV tools.


Formal Verification, Symbolic Model Verifier, Remote Procedure Call, Request protocol, Request Reply protocol, Request Reply Acknowledgement protocol