Module proper_statem

This module defines the proper_statem behaviour, useful for testing stateful reactive systems whose internal state and side-effects are specified via an abstract state machine.

Copyright 2010-2013 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas

Version: Apr 3 2013 10:43:12

Authors: Eirini Arvaniti.

Description

This module defines the proper_statem behaviour, useful for testing stateful reactive systems whose internal state and side-effects are specified via an abstract state machine. Given a callback module implementing the proper_statem behaviour (i.e. defining an abstract state machine of the system under test), PropEr can generate random symbolic sequences of calls to that system. As a next step, generated symbolic calls are actually performed, while monitoring the system's responses to ensure it behaves as expected. Upon failure, the shrinking mechanism attempts to find a minimal sequence of calls provoking the same error.

When including the "proper/include/proper.hrl" header file, all API functions of proper_statem are automatically imported, unless PROPER_NO_IMPORTS is defined.

The role of commands

Testcases generated for testing a stateful system are lists of symbolic API calls to that system. Symbolic representation has several benefits, which are listed here in increasing order of importance:

Since the actual results of symbolic calls are not known at generation time, we use symbolic variables (symb_var()) to refer to them. A command (command()) is a symbolic term, used to bind a symbolic variable to the result of a symbolic call. For example:

      [{set, {var,1}, {call,erlang,put,[a,42]}},
       {set, {var,2}, {call,erlang,erase,[a]}},
       {set, {var,3}, {call,erlang,put,[b,{var,2}]}}]

is a command sequence that could be used to test the process dictionary. In this example, the first call stores the pair {a,42} in the process dictionary, while the second one deletes it. Then, a new pair {b,{var,2}} is stored. {var,2} is a symbolic variable bound to the result of erlang:erase/1. This result is not known at generation time, since none of these operations is performed at that time. After evaluating the command sequence at runtime, the process dictionary will eventually contain the pair {b,42}.

The abstract model-state

In order to be able to test impure code, we need a way to track its internal state (at least the useful part of it). To this end, we use an abstract state machine representing the possible configurations of the system under test. When referring to the model state, we mean the state of the abstract state machine. The model state can be either symbolic or dynamic:

The callback functions

The following functions must be exported from the callback module implementing the abstract state machine:

The property used

Each test consists of two phases:

These two phases are encapsulated in the following property, which can be used for testing the process dictionary:

      prop_pdict() ->
          ?FORALL(Cmds, proper_statem:commands(?MODULE),
                  begin
                      {_History, _State, Result} = proper_statem:run_commands(?MODULE, Cmds),
                      cleanup(),
                      Result =:= ok
                  end).

When testing impure code, it is very important to keep each test self-contained. For this reason, almost every property for testing stateful systems contains some clean-up code. Such code is necessary to put the system in a known state, so that the next test can be executed independently from previous ones.

Parallel testing

After ensuring that a system's behaviour can be described via an abstract state machine when commands are executed sequentially, it is possible to move to parallel testing. The same state machine can be used to generate command sequences that will be executed in parallel to test for race conditions. A parallel testcase (parallel_testcase()) consists of a sequential and a parallel component. The sequential component is a command sequence that is run first to put the system in a random state. The parallel component is a list containing 2 command sequences to be executed in parallel, each of them in a separate newly-spawned process.

Generating parallel test cases involves the following actions. Initially, we generate a command sequence deriving information from the abstract state machine specification, as in the case of sequential statem testing. Then, we parallelize a random suffix (up to 12 commands) of the initial sequence by splitting it into 2 subsequences that will be executed concurrently. Limitations arise from the fact that each subsequence should be a valid command sequence (i.e. all commands should satisfy preconditions and use only symbolic variables bound to the results of preceding calls in the same sequence). Furthermore, we apply an additional check: we have to ensure that preconditions are satisfied in all possible interleavings of the concurrent tasks. Otherwise, an exception might be raised during parallel execution and lead to unexpected (and unwanted) test failure. In case these constraints cannot be satisfied for a specific test case, the test case will be executed sequentially. Then an f is printed on screen to inform the user. This usually means that preconditions need to become less strict for parallel testing to work.

After running a parallel testcase, PropEr uses the state machine specification to check if the results observed could have been produced by a possible serialization of the parallel component. If no such serialization is possible, then an atomicity violation has been detected. In this case, the shrinking mechanism attempts to produce a counterexample that is minimal in terms of concurrent operations. Properties for parallel testing are very similar to those used for sequential testing.

      prop_parallel_testing() ->
          ?FORALL(Testcase, proper_statem:parallel_commands(?MODULE),
                  begin
                      {_Sequential, _Parallel, Result} = proper_statem:run_parallel_commands(?MODULE, Testcase),
                      cleanup(),
                      Result =:= ok
                  end).
Please note that the actual interleaving of commands of the parallel component depends on the Erlang scheduler, which is too deterministic. For PropEr to be able to detect race conditions, the code of the system under test should be instrumented with erlang:yield/0 calls to the scheduler.

Data Types

command()

command() = {set, symb_var(), symb_call()}
          | {init, symbolic_state()}

command_list()

command_list() = [command()]

dynamic_state()

abstract datatype: dynamic_state()

fun_name()

fun_name() = atom()

history()

history() = [{dynamic_state(), term()}]

mod_name()

mod_name() = atom()

parallel_history()

parallel_history() = [{command(), term()}]

parallel_testcase()

parallel_testcase() = {command_list(), [command_list()]}

statem_result()

statem_result() = ok
                | initialization_error
                | {precondition, false | proper:exception()}
                | {postcondition, false | proper:exception()}
                | proper:exception()
                | no_possible_interleaving

symb_call()

symb_call() = {call, mod_name(), fun_name(), [term()]}

symb_var()

symb_var() = {var, pos_integer()}

symbolic_state()

abstract datatype: symbolic_state()

Function Index

behaviour_info/1Specifies the callback functions that should be exported from a module implementing the proper_statem behaviour.
command_names/1Extracts the names of the commands from a given command sequence, in the form of MFAs.
commands/1A special PropEr type which generates random command sequences, according to an absract state machine specification.
commands/2Similar to commands/1, but generated command sequences always start at a given state.
more_commands/2Increases the expected length of command sequences generated from CmdType by a factor N.
parallel_commands/1A special PropEr type which generates parallel testcases, according to an absract state machine specification.
parallel_commands/2Similar to parallel_commands/1, but generated command sequences always start at a given state.
run_commands/2Evaluates a given symbolic command sequence Cmds according to the state machine specified in Mod.
run_commands/3 Similar to run_commands/2, but also accepts an environment, used for symbolic variable evaluation during command execution.
run_parallel_commands/2Runs a given parallel testcase according to the state machine specified in Mod.
run_parallel_commands/3Similar to run_parallel_commands/2, but also accepts an environment used for symbolic variable evaluation, exactly as described in run_commands/3.
state_after/2Returns the symbolic state after running a given command sequence, according to the state machine specification found in Mod.
zip/2Behaves like lists:zip/2, but the input lists do no not necessarily have equal length.

Function Details

behaviour_info/1

behaviour_info(Attribute :: callbacks) -> [{fun_name(), arity()}]

Specifies the callback functions that should be exported from a module implementing the proper_statem behaviour.

command_names/1

command_names(Cmds :: command_list()) -> [mfa()]

Extracts the names of the commands from a given command sequence, in the form of MFAs. It is useful in combination with functions such as proper:aggregate/2 in order to collect statistics about command execution.

commands/1

commands(Mod :: mod_name()) -> proper_types:type()

A special PropEr type which generates random command sequences, according to an absract state machine specification. The function takes as input the name of a callback module, which contains the state machine specification. The initial state is computed by Mod:initial_state/0.

commands/2

commands(Mod :: mod_name(), InitialState :: symbolic_state()) ->
            proper_types:type()

Similar to commands/1, but generated command sequences always start at a given state. In this case, the first command is always {init,InitialState} and is used to correctly initialize the state every time the command sequence is run (i.e. during normal execution, while shrinking and when checking a counterexample). In this case, Mod:initial_state/0 is never called.

more_commands/2

more_commands(N :: pos_integer(), CmdType :: proper_types:type()) ->
                 proper_types:type()

Increases the expected length of command sequences generated from CmdType by a factor N.

parallel_commands/1

parallel_commands(Mod :: mod_name()) -> proper_types:type()

A special PropEr type which generates parallel testcases, according to an absract state machine specification. The function takes as input the name of a callback module, which contains the state machine specification. The initial state is computed by Mod:initial_state/0.

parallel_commands/2

parallel_commands(Mod :: mod_name(),
                  InitialState :: symbolic_state()) ->
                     proper_types:type()

Similar to parallel_commands/1, but generated command sequences always start at a given state.

run_commands/2

run_commands(Mod :: mod_name(), Cmds :: command_list()) ->
                {history(), dynamic_state(), statem_result()}

Evaluates a given symbolic command sequence Cmds according to the state machine specified in Mod. The result is a triple of the form
{History, DynamicState, Result}, where:

run_commands/3

run_commands(Mod :: mod_name(),
             Cmds :: command_list(),
             Env :: proper_symb:var_values()) ->
                {history(), dynamic_state(), statem_result()}

Similar to run_commands/2, but also accepts an environment, used for symbolic variable evaluation during command execution. The environment consists of {Key::atom(), Value::term()} pairs. Keys may be used in symbolic variables (i.e. {var,Key}) whithin the command sequence Cmds. These symbolic variables will be replaced by their corresponding Value during command execution.

run_parallel_commands/2

run_parallel_commands(Mod :: mod_name(),
                      Testcase :: parallel_testcase()) ->
                         {history(),
                          [parallel_history()],
                          statem_result()}

Runs a given parallel testcase according to the state machine specified in Mod. The result is a triple of the form
{Sequential_history, Parallel_history, Result}, where:

run_parallel_commands/3

run_parallel_commands(Mod :: mod_name(),
                      X2 :: parallel_testcase(),
                      Env :: proper_symb:var_values()) ->
                         {history(),
                          [parallel_history()],
                          statem_result()}

Similar to run_parallel_commands/2, but also accepts an environment used for symbolic variable evaluation, exactly as described in run_commands/3.

state_after/2

state_after(Mod :: mod_name(), Cmds :: command_list()) ->
               symbolic_state()

Returns the symbolic state after running a given command sequence, according to the state machine specification found in Mod. The commands are not actually executed.

zip/2

zip(A :: [A], B :: [B]) -> [{A, B}]

Behaves like lists:zip/2, but the input lists do no not necessarily have equal length. Zipping stops when the shortest list stops. This is useful for zipping a command sequence with its (failing) execution history.


Generated by EDoc, Apr 3 2013, 10:43:12.