×

zbMATH — the first resource for mathematics

Automated test case generation for the paxos single-decree protocol using a coloured Petri net model. (English) Zbl 1423.68319
Summary: Implementing test suites for distributed software systems is a complex and time-consuming task due to the number of test cases that need to be considered in order to obtain high coverage. We show how a formal Coloured Petri Net model can be used to automatically generate a suite of test cases for the Paxos distributed consensus protocol. The test cases cover both normal operation of the protocol as well as failure injection. To evaluate our model-based testing approach, we have implemented the Paxos protocol in the Go programming language using the quorum abstractions provided by the Gorums framework. Our experimental evaluation shows that we obtain high code coverage for our Paxos implementation using the automatically generated test cases.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68M12 Network protocols
68M14 Distributed systems
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
Software:
go; ZooKeeper
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Jepsen, Distributed systems safety analysis
[2] Utting, M.; Legeard, B., Practical Model-Based Testing: A Tools Approach, (2010), Elsevier
[3] Jensen, K.; Kristensen, L. M., Coloured Petri Nets: a graphical language for modelling and validation of concurrent systems, Commun. ACM, 58, 6, 61-70, (2015)
[4] CPN Tools, CPN Tools homepage, (2017)
[5] Kristensen, L. M.; Simonsen, K. I.F., Applications of Coloured Petri Nets for Functional Validation of Protocol Designs, 56-115, (2013), Springer · Zbl 1382.68151
[6] Liu, J.; Ye, X.; Li, J., Colored Petri Nets model based conformance test generation, (IEEE Symp. on Computers and Communications. IEEE Symp. on Computers and Communications, ISCC, (2011), IEEE), 967-970
[7] Wu, D.; Schnieder, E.; Krause, J., Model-based test generation techniques verifying the on-board module of a satellite-based train control system model, (2013 IEEE Intl. Conf. on Intelligent Rail Transportation Proceedings, (2013)), 274-279
[8] Zheng, W.; Liang, C.; Wang, R.; Kong, W., Automated test approach based on all paths covered optimal algorithm and sequence priority selected algorithm, IEEE Trans. Intell. Transp. Syst., 15, 6, 2551-2560, (2014)
[9] Kristensen, L. M.; Veiset, V., Transforming CPN models into code for TinyOS: a case study of the RPL protocol, (Proc. of ICATPN’16. Proc. of ICATPN’16, Lecture Notes in Computer Science, vol. 9698, (2016), Springer), 135-154
[10] MBT/CPN repository, (Aug 2018)
[11] Lamport, L., The part-time parliament, ACM Trans. Comput. Syst., 16, 2, 133-169, (1998)
[12] Lamport, L., Fast Paxos, Distrib. Comput., 19, 2, 79-103, (2006) · Zbl 1266.68218
[13] Lamport, L.; Malkhi, D.; Zhou, L., Vertical Paxos and primary-backup replication, (Proceedings of the 28th ACM Symp. on Principles of Distributed Computing. Proceedings of the 28th ACM Symp. on Principles of Distributed Computing, PODC ’09, (2009), ACM: ACM Calgary, AB, Canada), 312-313
[14] Moraru, I.; Andersen, D. G.; Kaminsky, M., There is more consensus in egalitarian parliaments, (ACM SIGOPS 24th Symp. on Operating Systems Principles. ACM SIGOPS 24th Symp. on Operating Systems Principles, SOSP ’13, (2013))
[15] Meling, H.; Marzullo, K.; Mei, A., When you don’t trust clients: Byzantine proposer fast Paxos, (32nd IEEE International Conference on Distributed Computing Systems. 32nd IEEE International Conference on Distributed Computing Systems, ICDCS, (2012), IEEE), 193-202
[16] Burrows, M., The Chubby lock service for loosely-coupled distributed systems, (Proc. of the 7th Symp. on Operating Systems Design and Implementation. Proc. of the 7th Symp. on Operating Systems Design and Implementation, OSDI ’06, (2006), USENIX Association), 335-350
[17] Bacon, D. F.; Bales, N.; Bruno, N.; Cooper, B. F.; Dickinson, A.; Fikes, A.; Fraser, C.; Gubarev, A.; Joshi, M.; Kogan, E.; Lloyd, A.; Melnik, S.; Rao, R.; Shue, D.; Taylor, C.; van der Holst, M.; Woodford, D., Spanner: becoming a SQL system, (Proc. of the 2017 ACM Intl. Conf. on Management of Data. Proc. of the 2017 ACM Intl. Conf. on Management of Data, SIGMOD ’17, (2017), ACM: ACM Chicago, Illinois, USA), 331-343
[18] Newcombe, C.; Rath, T.; Zhang, F.; Munteanu, B.; Brooker, M.; Deardeuff, M., How Amazon web services uses formal methods, Commun. ACM, 58, 4, 66-73, (2015)
[19] Meling, H.; Jehl, L., Tutorial summary: Paxos explained from scratch, (Baldoni, R.; Nisse, N.; van Steen, M., 17th International Conference on Principles of Distributed Systems. 17th International Conference on Principles of Distributed Systems, OPODIS. 17th International Conference on Principles of Distributed Systems. 17th International Conference on Principles of Distributed Systems, OPODIS, Lecture Notes in Computer Science, vol. 8304, (2013), Springer), 1-10
[20] Lea, T. E.; Jehl, L.; Meling, H., Towards new abstractions for implementing quorum-based systems, (Proc. of 37th IEEE Intl. Conf. on Distributed Computing Systems. Proc. of 37th IEEE Intl. Conf. on Distributed Computing Systems, ICDCS, (2017)), 2380-2385
[21] CPN testing model of the single-decree Paxos, (March 2018)
[22] Lamport, L., Paxos made simple, ACM SIGACT News, 32, 4, 18-25, (2001)
[23] Martin, J.-P.; Alvisi, L., Fast Byzantine consensus, IEEE Trans. Dependable Secure Comput., 3, 3, 202-215, (2006)
[24] Fischer, M. J.; Lynch, N. A.; Paterson, M. S., Impossibility of distributed consensus with one faulty process, J. ACM, 32, 2, 374-382, (1985) · Zbl 0629.68027
[25] Chandra, T. D.; Hadzilacos, V.; Toueg, S., The weakest failure detector for solving consensus, J. ACM, 43, 685-722, (1996) · Zbl 0885.68022
[26] Attiya, H.; Bar-Noy, A.; Dolev, D., Sharing memory robustly in message-passing systems, J. ACM, 42, 1, 124-142, (1995) · Zbl 0886.68018
[27] Jehl, L.; Vitenberg, R.; Meling, H., SmartMerge: a new approach to reconfiguration for atomic storage, (Moses, Y., Distributed Computing - 29th Intl. Symp.. Distributed Computing - 29th Intl. Symp., DISC 2015. Distributed Computing - 29th Intl. Symp.. Distributed Computing - 29th Intl. Symp., DISC 2015, Lecture Notes in Computer Science, vol. 9363, (2015), Springer), 154-169
[28] Vukolić, M., Quorum Systems: With Applications to Storage and Consensus, Synthesis Lectures on Distributed Computing Theory, vol. 3 (1), (2012), Morgan & Claypool Publishers
[29] Google Inc., gRPC remote procedure calls
[30] Google Inc., Protocol buffers
[31] Grieskamp, W.; Kicillof, N.; Stobie, K.; Braberman, V., Model-based quality assurance of protocol documentation: tools and methodology, Softw. Test. Verif. Reliab., 21, 1, 55-71, (2011)
[32] Meling, H., A framework for experimental validation and performance evaluation in fault tolerant distributed system, (Workshop on Dependable Parallel, Distributed and Network-Centric Systems. Workshop on Dependable Parallel, Distributed and Network-Centric Systems, DPDNS, (2007), IEEE), 1-8
[33] Chandra, T. D.; Griesemer, R.; Redstone, J., Paxos made live: an engineering perspective, (Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Distributed Computing. Proceedings of the Twenty-Sixth Annual ACM Symposium on Principles of Distributed Computing, PODC ’07, (2007), ACM), 398-407
[34] Artho, C.; Gros, Q.; Rousset, G.; Banzai, K.; Ma, L.; Kitamura, T.; Hagiya, M.; Tanabe, Y.; Yamamoto, M., Model-based API testing of apache ZooKeeper, (2017 IEEE Intl. Conf. on Software Testing, Verification and Validation. 2017 IEEE Intl. Conf. on Software Testing, Verification and Validation, ICST, (2017)), 288-298
[35] Ponce de León, H.; Haar, S.; Longuet, D., Model-based testing for concurrent systems: unfolding-based test selection, Int. J. Softw. Tools Technol. Transf., 18, 3, 305-318, (2016)
[36] Hawblitzel, C.; Howell, J.; Kapritsos, M.; Lorch, J.; Parno, B.; Roberts, M. L.; Setty, S.; Zill, B., IronFleet: proving practical distributed systems correct, (Proceedings of the ACM Symposium on Operating Systems Principles. Proceedings of the ACM Symposium on Operating Systems Principles, SOSP, (2015), ACM)
[37] Padon, O.; Losa, G.; Sagiv, M.; Shoham, S., Paxos made EPR: decidable reasoning about distributed protocols, Proc. ACM Program. Lang., 1, 108:1-108:31, (2017)
[38] Fonseca, P.; Zhang, K.; Wang, X.; Krishnamurthy, A., An empirical study on the correctness of formally verified distributed systems, (Proc. of the Twelfth European Conf. on Computer Systems, (2017), ACM), 328-343
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.