Tomasz Kowal, tech lead at ClubCollect, presented at Lambda Days 2019 an introduction to stateful property based testing. Property-based testing helped major companies find bugs which were not caught through example-based testing. Stateful property-based testing leverages an underlying model of the system under test to generate interesting test sequences, increasing the likelihood of finding bugs.
To illustrate the practical value of property-based testing, Kowal details how three companies found bugs in their systems, which were not found through example-based methods.
Quviq, the author the QuickCheck property-based testing tool, tested the AUTOSAR system for Volvo, the car manufacturer. AUTOSAR creates a high-level function bus that connects electronic control units (ECUs) within a vehicle in a protocol agnostic way. Stringent certification requirements in the automobile industry result in the necessity to thoroughly test embedded devices and the system connecting them. While the embedded devices were individually tested by their respected teams, property-based testing allowed Quviq to find an undetected erroneous behaviour: when the volume of the radio was turned up or down, the brakes did not work. This bug was found within a week, after developing a model of the system under test. The root issue turned out to be with different Endianess used in different parts of the system. Radio operations which had the smallest priority of all actions, turned out to acquire a higher priority than brakes operations due to a change of Endianess (cf. Little Endian vs. Big Endian).
Google’s LevelDB key-value store had a recurrent issue with phantom keys. After modeling the database and using property-based testing, Google found reproducible examples leading to the ghost key issue. The minimal example consisted of 17 consecutive operations. While such an example is large enough to not come up in unit tests generated by human testers, it is short enough to be checked against, to identify the root cause for the behaviour.
The last example deals with DropBox and involves testing distributed, highly-concurrent software. By modelizing the behaviour of DropBox along all the possible non-deterministic order of incoming operations, researchers were able to identify ordering of operations which led to loss of data.
Kowal signals the lack of intermediate-level resources explaining how to practically use property-based testing in everyday software. Most of commonly known resources are either too simplistic (testing simple data structures), thus understating the scope of applicability of the technique, or summarily illustrate epic wins for large software and complex systems, like the aforementioned examples.
Property-based testing (PBT) relies on properties which can be written in pseudocode as:
for all (x, y, ...)
such as precondition(x, y, ...) holds
property(x, y, ...) is true
Introductory examples usually illustrate the technique with testing a data structure or a function, by recording its inputs and outputs and checking that specified properties are all valid.
Few commonly known examples deal with stateful PBT applied to testing actual live systems. In his talk, Kowal gives such an example. The process involves the identification of properties, building a stateful model of the system under test (SUT), using that model to generate interesting test sequences, running the test sequences on the actual system, comparing at each step of the run the system behaviour and outputs to those predicted by the model, and shrinking failing test sequences to a minimal expression.
To help identifying properties, Scott Wlaschin, senior software architect and maintainer of a popular F# learning resource, suggests an orientative taxonomy of properties:
- Different paths, same destination
- There and back again
- Some things never change
- The more things change, the more they stay the same
- Solve a smaller problem first
- Hard to prove, easy to verify
- The test oracle
Generating good test sequences which are more likely to find bugs is critical in the success of any testing method. In the example given in the talk, a patient database is modeled by a key-value store, which handle two commands: search a patient, and add a patient. A naive generation of test sequences results in sequences containing any number of the two commands in any order, involving patients which are unrelated:
search(p1)
add(p2, name1, surname1)
search(p3)
add(p4, name2, surname2)
More interesting sequences can be generated by adding state to the test sequence generation process. This allows for smarter commands which take past test inputs into account:
Search for existing patient
Search missing patient
Add new patient
Add patient who already exists
While the example Kowal discusses is presented with Erlang as a base language, the technique is applicable to any language, including JavaScript.
The full video recorded at Lambda Days 2019 is available online. Lambda Days is a developer conference focusing on functional programming methods and techniques. Lambda Days 2020 will be held the 13th and 14th of February 2020 in Kraków, Poland.
