Formal Modeling and Verifying Dubbo Using Process Algebra

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 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 five properties are valid, including Deadlock Freedom, Connectivity, Robustness, Parallelism and Consistency. 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.