Model-based software testing for distributed systems and protocols

Abstract

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.