Extension of the test pyramid through model checking - Part 1


With the microservices and serverless trends, and the increased use of eventually consistent databases, development teams will increasingly face the challenges of distributed systems. This article deals with two specific categories of errors that are particularly provoked by distributed systems: Consistency errors and concurrency errors.

These types of errors are particularly hard to reproduce, can lead to unnoticed data corruption and are difficult to identify with established testing procedures.

In the upcoming series of articles we will look at two types of consistency errors and one type of concurrency error. We will discover that the tools of the test pyramid alone are insufficient to detect these types of errors and will therefore use model checking as an extension to the test pyramid. We develop an idea how to model a distributed and concurrent system and test for these types of errors automatically. Subsequently, we have a look at an optimized tool that allows the reader to apply the presented techniques in his projects.

The test pyramid in agile software development

Agile software development requires a high level of technical quality of the software increment. In particular, this includes automated testing of the software at the source code level (unit tests), in a network of components (integration tests) and from the customer's perspective (end-to-end tests). The recommended number of test from each test category is illustrated by the test pyramid:

The term test pyramid reflects the broad consensus within the agile development community that the best cost-value ratio of tests leads to a distribution of unit tests to integration tests and end-to-end tests to the shape of a pyramid.

The tools of the test pyramid

The tools of the test pyramid consists of three types of tests:

Unit Tests

Given that they meet the FIRST criteria, unit tests provide the fastest and most reliable feedback:

  • Fast: Unit tests should be fast

  • Isolated: Unit tests should be independent of external dependencies like a database

  • Repeatable: Unit tests should be repeatable, i.e. deterministic

  • Self Validating: Unit Test should result in a clear-cut conclusion

  • Timely: You should write unit tests as early as possible, preferably before the production code

End-To-End Tests

Although end-to-end tests provide the slowest feedback and their maintenance is the most time-consuming, these tests are the closest to reality. End-to-end testing uses the same testing capabilities as a human tester or a user of the system.

Integrations Tests

Integration tests represent a middle way between unit tests and end-to-end tests. Integration testing is used to test the technical interaction of components or services, but not via the user interface of the system, but in an artificially created test setup, similar to unit tests. The setup is less artificial than with unit tests, but not as realistic as with end-to-end tests.

Extension of the test pyramid through model checking

The FIRST criteria make it clear that unit tests are the wrong tool for both consistency and concurrency errors. Suppose you want to test a system that uses a database with the consistency model "Eventual Consistency" for consistency errors. Since a unit test, due to the Isolated criterion, must not have a dependency on a database, the system cannot be tested in a unit test in interaction with the database. The workaround of using a fake database instead would only lead to a false sense of security, since the behavior of the database cannot be exactly simulated in many respects. Unit tests are also unsuitable for testing concurrency, since concurrency problems occur mainly randomly and indeterministically. However, it is precisely these properties that the repeatability criterion excludes.

For integration tests, and even more so for end-to-end tests, the combination of possible setups, steps and constellations at this level leads to such a high number of test combinations that the probability of detecting consistency and concurrency errors is low. Integration testing is the most likely way to reproduce consistency or concurrency errors, but even this is often difficult and time-consuming.

Model checking of a distributed and concurrent system is an extension of the tools of the test pyramid to reliably prevent consistency and concurrency errors. Modeling in this context means abstracting from the concrete code and focusing on the behavior and properties of the system. For this purpose, the following questions are asked:

  1. Which events can occur?

  2. What is the state of the system after a particular event?

  3. What condition must the system fulfill at all times?

The answers to these questions form a model of the system under test. A model checker can use it to generate any combination of events and automatically test whether the required conditions for the state of the system are fulfilled after each event. If the model checker finds a violation of a condition, a logical error in the design of the system has been found. If the model checker does not find an error, the design of the system fulfills the formulated conditions and the translation of the design into the desired programming language and runtime environment can begin. Since translation errors can still occur during the implementation of the design, using the tools of the test pyramid is still crucial.

To demonstrate the benefits and concrete application of model checking, two examples are discussed in the following posts. The first example checks a distributed system for consistency violations, the second example shows how to identify and exclude concurrency errors.