kiri-check Help

Stateful testing

What should be tested

In stateful testing, the validity of the behavior of a stateful system is examined. Random operations, called commands, are repeatedly executed on the real system, and the states before and after these operations are compared with those of a separately implemented model.

If an error occurs during execution or the comparison with the model is invalid, shrinking is performed similarly to stateless testing. Shrinking in stateful testing aims to find the minimal combination of commands and values that cause the failure.

Execution model

In stateful testing, tests are divided into multiple cycles. Each cycle consists of initializing the state and system, performing steps of random commands, and verifying the postconditions of commands.

Each cycle is executed in two phases. The first phase involves generating the commands to be executed, and the second phase involves executing these commands. In the second phases, if an error occurs or a check fails, shrinking begins.

Command generation phase

In the command generation phase, commands to be executed are randomly generated. This phase only involves the model, and the real system is not yet created.

The following diagram illustrates the command generation phase:

true
false
Behavior.initializeState()
Behavior.initializePrecondition(State)
if_init_precond
Behavior.generateCommands(State)
Fail
Command selection loop
true
false
Randomly select
Command.precondition(State)
Command.nextState(State)
Skip

The process begins with Behavior.initializeState(), which generates the model. This method, initializeState(), should be defined by the user. The generated instance is then checked for initialization preconditions using Behavior.initializePrecondition(State). If the return value is false, the test fails. initializePrecondition() is a method that can be defined by the user and by default returns true. It is important that no destructive changes are made during this check.

Next, Behavior.generateCommands(State) generates a list of commands to be executed. This method allows the model object to be referenced during generation and should be defined by the user. The commands to be used are determined in the subsequent loop.

The command selection loop begins, where commands are selected from the generated list. A command is randomly chosen, and Command.precondition(State) is executed for that command. If the return value is false, the process skips to the next command selection. The model can be referenced during this check, and no destructive changes should be made.

If the precondition check passes, Command.nextState(State) is executed to change the state of the model according to the command. This loop continues until the specified number of commands has been selected and executed.

Execution phase

In the execution phase, the generated commands are applied to the real system for testing.

The following diagram illustrates the execution phase:

true
false
Behavior.initializeState()
Behavior.initializePrecondition(State)
Behavior.createSystem(State)
Fail
Execution loop
true
false
Pass the return value
true
false
Command.precondition(State)
Command.run(System)
Shrinking
Command.postcondition(State, Result)
Command.nextState(State)
Behavior.destroy(System)

The process up to Behavior.initializePrecondition(State) is the same as in the command generation phase. Behavior.createSystem(State) then generates the real system. Next, the list of commands generated in the command generation phase is executed in sequence.

First, Command.precondition(State) checks the precondition of the command. Unlike the command generation phase, if the result is false, shrinking begins. Since the situation is different from the command generation phase, it is possible for a command to fail here. No destructive changes should be made.

Command.run(System) is executed to manipulate the real system. If the command uses arbitraries, the generated values are also used. If any exception occurs, shrinking begins. The return value is used in the next step (postcondition check).

Command.postcondition(State, Result) is executed to check the postcondition. If the result is false, shrinking begins. The postcondition verifies the expected state of the model against the real system after the command execution, or compares the differences between the two. If there are no issues, it returns true; otherwise, it returns false and shrinking begins. The model and the return value of run are used to check the postcondition.

If the command uses arbitraries, the same values used in run are referenced. Note that the postcondition is checked before nextState is called. At this point, the state of the model is the same as before the command execution in the real system. No destructive changes should be made to the model. nextState will be called afterward.

Finally, Command.nextState(State) progresses the state of the model. The process ends when all commands are executed or shrinking completes.

Shrinking

When an error occurs, the test initiates a process called shrinking. The goal of shrinking is to identify the minimal sequence of commands that causes the failure. This process is divided into three phases.

First, the sequence of commands that caused the error is split into several partial sequences. This allows us to determine which partial sequence still causes the error. In the diagram below, the original sequence of commands is divided into three partial sequences. Each partial sequence is tested to see if the error can be reproduced, and the partial sequence that reproduces the error is carried forward to the next phase.

Next, the selected partial sequence is further reduced by removing unnecessary commands to identify the minimal sequence that causes the error. In this phase, commands within the partial sequence are removed one by one to see which combinations still cause the error. The diagram shows how the sequence is minimized to identify the smallest sequence that still causes the error.

Finally, the arguments or generated values of the commands are shrunk. In this phase, the values used in the commands are reduced or simplified to see if the error still occurs. This helps identify the minimal combination of values that causes the error. The example in the diagram shows the final shrunk values.

The following diagram illustrates the process from error occurrence to shrinking, ultimately identifying the minimal sequence of commands that causes the error:

Split into sequences
Fail: 2 4 4 6
Minimum sequence: 2 6
Falsifying sequence with minimum values
6
2
Phase 2: Reduced sequences
Reduced: 6
4
2
4
Reduced: 2
6
4
4
Reduced: 4
6
2
Phase 1: Partial sequences
7
2
8
1
3
1
5
7
6
2
4
4
Failed sequence
7
1
5
7
3
2
4
4
6
2
8
1
Phase 3: Shrinking values
Last modified: 13 September 2024