SpringerLink
Log in

Formal Modeling and Verifying Dubbo Using Process Algebra

  • Published:
Mobile Networks and Applications Aims and scope Submit manuscript

Abstract

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8

Similar content being viewed by others

Data Availability

Not Applicable.

References

  1. Bao C (2022) Enterprise informatization construction and management mode feedback platform design based on dubbo architecture and concurrency computation. In: 2022 International Conference on Edge Computing and Applications (ICECAA), IEEE, pp 1521–1524

  2. Baptista T, Silva LB, Costa C (2021) Highly scalable medical imaging repository based on kubernetes. In: 2021 IEEE International Conference on Bioinformatics and Biomedicine (BIBM), IEEE, pp 3193–3200

  3. Birrell AD, Nelson BJ (1984) Implementing remote procedure calls. ACM Trans Comput Syst (TOCS) 2(1):39–59

    Article  Google Scholar 

  4. Brewer EA (2015) Kubernetes and the path to cloud native. In: Proceedings of the sixth ACM symposium on cloud computing, pp 167–167

  5. Cao L, Sharma P (2021) Co-locating containerized workload using service mesh telemetry. In: Proceedings of the 17th International Conference on emerging Networking EXperiments and Technologies, pp 168–174

  6. Chen N, Zhu H, Yin J, Fei Y, **ao L, Zhu M (2022) Modeling and verifying ndn-based iov using csp. Journal of Software: Evolution and Process 34(10):e2371

    Google Scholar 

  7. CNCF Cloud Native Definition v10 (2023) [Online] Available. https://github.com/cncf/toc/blob/main/DEFINITION.md

  8. Dab B, Fajjari I, Rohon M, Auboin C, Diquélou A (2020) Cloud-native service function chaining for 5g based on network service mesh. In: ICC 2020-2020 IEEE International Conference on Communications (ICC), IEEE, pp 1–7

  9. Dähling S, Razik L, Monti A (2021) Enabling scalable and fault-tolerant multi-agent systems by utilizing cloud-native computing. Auton Agent Multi-Agent Syst 35(1):1–27

    Article  Google Scholar 

  10. Dubbo (2023) [Online] Available. http://dubbo.apache.org

  11. Dubbo 30 forward-looking docking of Kubernetes native services (2023) [Online] Available. https://www.kubernetes.org.cn/8852.html

  12. ETCD (2023) [Online] Available. https://etcd.io/

  13. Hoare CAR (1978) Communicating sequential processes. Communications of the ACM 21(8):666–677

    Article  MATH  Google Scholar 

  14. Hou Z, Yin J, Zhu H (2021) Formalization and verification of dubbo using CSP. In: The 33rd International Conference on Software Engineering and Knowledge Engineering, SEKE 2021, KSIR Virtual Conference Center, USA, July 1 -July 10, 2021, KSI Research Inc., pp 154–159

  15. HSF (2023) [Online] Available. https://help.aliyun.com/document_detail/100087.html

  16. Hussain F, Li W, Noye B, Sharieh S, Ferworn A (2019) Intelligent service mesh framework for api security and management. In: 2019 IEEE 10th Annual Information Technology, Electronics and Mobile Communication Conference (IEMCON), IEEE, pp 0735–0742

  17. Jiang X, Hu Y, **ang Y, Jiang G, ** X, **a C, Jiang W, Yu J, Wang H, Jiang Y et al (2020) Alibaba hologres: A cloud-native service for hybrid serving/analytical processing. Proceedings of the VLDB Endowment 13(12):3272–3284

    Article  Google Scholar 

  18. Josuttis NM (2007) SOA in practice: the art of distributed system design. “O’Reilly Media, Inc.”

  19. Kratzke N, Quint PC (2017) Understanding cloud-native applications after 10 years of cloud computing-a systematic map** study. J Syst Softw 126:1–16

    Article  Google Scholar 

  20. Kummert H (1998) The ppp triple-des encryption protocol (3dese). Tech. rep

  21. Li F (2019) Cloud-native database systems at alibaba: Opportunities and challenges. Proceedings of the VLDB Endowment 12(12):2263–2272

    Article  Google Scholar 

  22. Li W, Lemieux Y, Gao J, Zhao Z, Han Y (2019) Service mesh: Challenges, state of the art, and future research opportunities. In: 2019 IEEE International Conference on Service-Oriented System Engineering (SOSE), IEEE, pp 122–1225

  23. Liu A, Zhu H, Popovic M, **ang S, Zhang L (2020) Formal analysis and verification of the pstm architecture using csp. J Syst Softw 165(110):559

    Google Scholar 

  24. Lowe G, Roscoe B (1997) Using csp to detect errors in the tmn protocol. IEEE Trans Softw Eng 23(10):659–669

    Article  Google Scholar 

  25. Marchese A, Tomarchio O (2022) Extending the kubernetes platform with network-aware scheduling capabilities. In: International Conference on Service-Oriented Computing, Springer, pp 465–480

  26. Merenstein A, Tarasov V, Anwar A, Bhagwat D, Lee J, Rupprecht L, Skourtis D, Yang Y, Zadok E (2021) \(\{\)CNSBench\(\}\): A cloud native storage benchmark. In: 19th USENIX Conference on File and Storage Technologies (FAST 21), pp 263–276

  27. Microservices (2023) [Online] Available. https://martinfowler.com/articles/microservices.html

  28. Motan (2023) [Online] Available. https://github.com/weibocom/motan

  29. Netto HV, Lung LC, Correia M, Luiz AF, de Souza LMS (2017) State machine replication in containers managed by kubernetes. J Syst Archit 73:53–59

    Article  Google Scholar 

  30. PAT (2023) [Online] Available. http://pat.comp.nus.edu.sg/

  31. Ponomarev KY (2019) Attribute-based access control in service mesh. 2019 Dynamics of Systems. Mechanisms and Machines (Dynamics), IEEE, pp 1–4

    Google Scholar 

  32. Roscoe A, Huang J (2013) Checking noninterference in timed csp. Form Asp Comput 25(1):3–35

    Article  MathSciNet  MATH  Google Scholar 

  33. Stine M (2015) Migrating to cloud-native application architectures. O’Reilly Media

  34. Sun J, Liu Y, Dong JS (2008) Model checking csp revisited: Introducing a process analysis toolkit. In: International symposium on leveraging applications of formal methods, verification and validation, Springer, pp 307–322

  35. Tars (2023) [Online] Available. https://tarscloud.org/

  36. The Distributed Service Framework (DSF) (2023) [Online] Available. https://github.com/dist-svc

  37. Van Steen M, Tanenbaum A (2002) Distributed systems principles and paradigms. Network 2:28

    MATH  Google Scholar 

  38. Vayghan LA, Saied MA, Toeroe M, Khendek F (2021) A kubernetes controller for managing the availability of elastic microservice based stateful applications. J Syst Softw 175(110):924

    Google Scholar 

  39. **ao L, Zhu H, Xu Q, Vinh PC (2022) Modeling and verifying pso memory model using csp. Mobile Networks and Applications, pp 1–16

  40. **ong S, Huang B (2021) A novel think tanks evaluation system based on micro service. In: Journal of Physics: Conference Series, IOP Publishing, vol 1757, p 012197

  41. Yi J, Lin L (2019) Deep understanding of Apache Dubbo and actual combat. “House of Electronics Industry.”

  42. Zhang Y, Liu Y, Li B, Li L (2019) Research on distribution network status management system based on cloud platform. 2019 International Joint Conference on Information. Media and Engineering (IJCIME), IEEE, pp 391–395

    Google Scholar 

  43. Zhao H, Jiang Y, Zhao X (2020) Design and research of university intelligent education cloud platform based on dubbo microservice framework. 2020 5th International Conference on Mechanical. Control and Computer Engineering (ICMCCE), IEEE, pp 870–874

    Google Scholar 

  44. Zookeeper (2023) [Online] Available. https://zookeeper.apache.org

Download references

Author information

Authors and Affiliations

  1. Shanghai Key Laboratory of Trustworthy Computing, East China Normal University, Shanghai, China

    Zhiru Hou & Huibiao Zhu

  2. School of Software, Northwestern Polytechnical University, **’an, China

    Jiaqi Yin

  3. Nguyen Tat Thanh University, 300A Nguyen Tat Thanh Street, Ward 13, District 4, Ho Chi Minh City, Vietnam

    Phan Cong Vinh

Authors
  1. Zhiru Hou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jiaqi Yin
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Huibiao Zhu
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Phan Cong Vinh
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Huibiao Zhu.

Ethics declarations

Competing interests

We have no competing interests to declare that are relevant to the content of this article. This article does not involve ethics issues.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Hou, Z., Yin, J., Zhu, H. et al. Formal Modeling and Verifying Dubbo Using Process Algebra. Mobile Netw Appl (2023). https://doi.org/10.1007/s11036-023-02181-z

Download citation

  • Accepted:

  • Published:

  • DOI: https://doi.org/10.1007/s11036-023-02181-z

Keywords

Search

Navigation