Formalization and verification of dubbo using CSP

Dubbo is a high-performance, lightweight Java Remote Procedure Call (RPC) framework developed by Alibaba, which provides interface-oriented remote method call, intelligent fault tolerance and automatic service registration. Since Dubbo is extensively applied recently as an excellent representative RPC framework, it is of great significance to formally analyze Dubbo. In this paper, we use Communicating Sequential Processes (CSP) to model and formalize Dubbo. In order to enhance the reliability of the call, we use token authentication mechanism in the modeling process. Moreover, we put the CSP description of the established model into the model checker Process Analysis Toolkit (PAT) for simulation and verification. We verify whether the four properties are valid, including Deadlock Freedom, Connectivity, Robustness and Parallelism. Our final verification results show that the model can satisfy these properties, thus we can conclude the framework can guarantee the highly available remote call.