PropEr is an open-source tool for automated random testing of Erlang function
properties from specifications. Its original focus was on testing pure
functions. Nevertheless, projects implemented in Erlang typically consist of
stateful code. In this thesis, we have extended PropEr with two library modules
that support random model-based testing of stateful reactive systems. The model
behaviour of the system under test should be defined in a callback module.
Given this model, we test a stateful system by generating and performing
sequences of calls to that system, while monitoring its actual responses to
ensure the system behaves as expected.

The first module, proper_statem, is designed to test generic servers and other
systems with stateful interfaces, whose side-effects are specified via an
abstract state machine. The same state machine specification can also be used
for generating sequences of calls that will be executed in parallel to test for
race conditions. The second module, proper_fsm, offers a convenient way to test
systems exhibiting a finite state machine behaviour, as it is designed to bring
the callback module specification very close to a state diagram. Defining a
model of the system under test is by no means a trivial task. To compensate for
that, we present detailed tutorials on effectively using the new library
modules to test stateful systems.