Wrapping Up

Summary

In this final chapter, we’ve seen how to bring stateful properties to the next level in cases where the system under test can be modeled as a finite state machine. In such cases, FSM properties represent a useful specialization mechanism that lets us generate calls and data according to the state in which the system should be. We’ve been through the data generation model (both symbolic and real) for the property and have put it all in practice through tests for Klarna’s circuit_breaker library. We came up with a multistate model, which proved to be ill-fitting for the actual library. We then went through the debugging steps required to fix the model and through the statistics collected in the test execution. Finally, we rebalanced the possible generated events to get better transition coverage.

What’s next

We now have all the knowledge required to use properties to find tricky bugs in all kinds of systems, from basic unit tests up to larger integration suites. We’re ready to go on and start adding better tests to our software, and improve software quality overall.