Model-based software testing for distributed systems and protocols
MetadataVis full innførsel
Society is increasingly dependent on fault-tolerant cloud-based services which rely on the correctness and reliability of advanced distributed software systems and consensus protocols. The implementations of these systems require complex processing logic which in turn makes them challenging to implement correctly and also challenging to test in a systematic way. Model-based software testing (MBT) is a powerful approach for testing software systems. MBT enables automated test case generation from models, which can be used to investigate fault-tolerance and expose errors in the implementations of software systems. The research idea underlying this thesis is to investigate the application of MBT for distributed software systems and protocols, with the aim of ensuring the correctness, reliability, and consistency of their implementations. This thesis contains scientific contributions in three main research areas of MBT for distributed systems. The first contribution is to investigate MBT for quorum-based fault-tolerant distributed systems. This has resulted in a general MBT approach and supporting QuoMBT framework based on generating test cases from models created via Coloured Petri Nets (CPNs). QuoMBT enables testing of the Gorums middleware framework and quorum-based fault-tolerant distributed systems implemented via Gorums. Our experimental evaluation shows that the QuoMBT framework can obtain high code coverage and successfully detect programming errors in the Gorums middleware and distributed systems implemented based on the Gorums framework. The second contribution has been to develop software tools and techniques to support MBT for distributed systems. We have developed the MBT/CPN software engineering tool for test case generation from models constructed using CPNs. The tool can perform both simulation and state space-based test case generation, and is important for practical application of MBT. The MBT/CPN tool has been successfully applied to test a distributed storage system and a Paxos consensus protocol both implemented via the Gorums framework. The general applicability of the tool has been demonstrated by validating the correctness of a two-phase commit transaction protocol. The third contribution involves two research directions. One is an approach to measure and visualize the execution path coverage criterion of test cases. The experimental results show that our abstraction-based visualization provides useful visual feedback of tests, their coverage and diversity. The other is a search-based test case generation technique based on multi-objective reinforcement learning and optimization. It relies on a bandit-based heuristic search strategy implemented to guide test case generation and a multi-objective optimization technique. We have performed an experimental evaluation on a collection of examples, including the ZooKeeper distributed coordination service. The results show that test cases generated using our search-based approach provide predictable and improved state- and transition coverage, find failures earlier, and provide increased path coverage.
Består avR.Wang, L. M. Kristensen, H. Meling, and V. Stolz. Model-Based Testing of the Gorums Framework for Fault-Tolerant Distributed Systems. In Transactions on Petri Nets and Other Models of Concurrency XIII, volume 11090 of Lecture Notes in Computer Science, pages 158–180, Springer International Publishing, 2018. https://doi.org/10.1007/978-3-662-58381-4_8
R. Wang, L. M. Kristensen, H. Meling, and V. Stolz. Automated test case generation for the Paxos single-decree protocol using a Coloured Petri Net model. In Journal of Logical and Algebraic Methods in Programming, volume 104, pages 254–273, Elsevier Ltd, 2019. https://doi.org/10.1016/j.jlamp.2019.02.004
R. Wang, L. M. Kristensen, and V. Stolz. MBT/CPN: A Tool for Model-Based Software Testing of Distributed Systems Protocols Using Coloured Petri Nets. In Verification and Evaluation of Computer and Communication Systems, volume 11181 of Lecture Notes in Computer Science, pages 97–113, Springer International Publishing, 2018. https://doi.org/10.1007/978-3-030-00359-3_7
R.Wang, C. Artho, L. M. Kristensen, and V. Stolz. Visualization and Abstractions for Execution Paths in Model-Based Software Testing. In Integrated Formal Methods, volume 11918 of Lecture Notes in Computer Science, pages 474–492, Springer International Publishing, 2019. https://doi.org/10.1007/978-3-030-34968-4_26
R. Wang, C. Artho, L. M. Kristensen, and V. Stolz. Multi-objective Search for Model-based Testing. Submitted to The 20th IEEE International Conference on Software Quality, Reliability, and Security, Vilnius, Lithuania, IEEE, 2020.