Society is heavily dependent on software and software systems, and design- and implementation errors in systems may render them unavailable and return erroneous results to the users. It is therefore important to develop automated techniques and supporting software tools that can be used to support the engineering of correct and stable software systems. This post summarizes the tools developed for an automated model-based software testing approach to validate implementations of distributed systems and protocols. These tools include:

1. an MBT/CPN software engineering tool (Github link) [1] developed as an extension for the CPN Tools [2] to automatically generate test cases.
2. a test execution engine (Github link) developed that has an adapter generator implemented in the Go programming language to automatically generate the test adapter that can perform test case execution the system under test.

The tools were used to validate the correctness of a two-phase commit transcation protocol (Github link) implemented in the Go programming language. The MBT/CPN tool was also used to test a distributed storage system [3] and a Paxos distributed consensus protocol [4] (see my another post).

Design

Software Architecture of the MBT/CPN Software Tool

The figure below shows the software architecture of the MBT/CPN Tool. The tool was developed on the top of the CPN Tool. This tool can automatically generate test cases in the XML format from CPN testing models using both simulation-based test case generation (SSTCG) and state space-based test case generation (SimTCG). The generated test cases can be read by a reader and executed by a tester of a test adapter to validate the correctness of the system under test.

Test Execution Engine

The figure below gives the overall process of using the test execution engine. When exporting test cases from the MBT/CPN tool into an XML file (step (1)), two elements of information are generated and inserted into the XML format. One element is test cases; the other element is the settings used to generate a Test Adapter. The information included in these settings is used by the adapter generator of the test execution engine which has predefined Go templates to generate a test adapter consisting of a reader and a tester in the Go programming language (step (2) and (3)). After the test adapter has been generated, the reader can read the information included in the test cases of the XML file (step (4)). Then, the tester can execute them against the system under test and compare the output of the SUT with expected output (oracle) (steps (5), (6) and (7)).

Implementation & development of software tools

• a two-phase commit transcation protocol was implemented as the system under test.
• the MBT/CPN tool was developed on the top of the CPN Tools.
• the test execution engine was developed in the Go programming language with Go templates implemented using the text/template and encoding/xml packages, both belonging to the Go standard library.
• the automated testing environment and test scripts were developed using shell scripting.

Testing & Evaluation

We successfully applied the MBT/CPN tool to test a distributed storage system and a Paxos consensus protocol both implemented via the Gorums framework (see my another post). The general use of the tool has been demonstrated by validating the correctness of a two-phase commit transaction protocol. The demonstrations have shown that the MBT/CPN tool can successfully support our MBT approach and test cases generated by the MBT/CPN tool yield high statement coverage and detect errors in the implementations.

References

1. 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.
2. CPN Tools. CPN Tools homepage.
3. 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.
4. R. 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.

Other related publications

1. R. Wang, L. M. Kristensen, H. Meling, and V. Stolz. Application of Model-based Testing on a Quorum-based Distributed Storage. In CEUR Workshop Proceedings, Petri Nets and Software Engineering (PNSE’17), volume 1846, pages 177–196, 2017.
2. R. Wang, L. M. Kristensen, H. Meling, and V. Stolz. Model-based Testing of the Gorums Framework for Fault-tolerant Distributed Systems. In Proceedings of the 29th Nordic Workshop on Programming Theory (NWPT), Turku Center for Computer Science, Finland, 2017.