Definition
Sequence testing is a testing approach in which tests describe sequences of state transitions that a system may perform. In contrast to unit-test-oriented generation, which uses preconditions and postconditions of individual system operations, sequence-test-oriented approaches use temporal specifications or automata-based specifications of system behavior. In processor test-program generation, the processor state is an important part of the test description, and tests describe sequences of state transitions caused by executing program instructions.
Relation to unit testing
In the VAMP processor case study, the authors distinguish model-based unit testing from sequence testing. A unit testing scenario is described by preconditions and postconditions on the inputs and results produced by the system under test, and it assumes access to the internal state after the test. A sequence testing scenario requires control of internal-state initialization and, in some cases, reference to the final state; the test result is inferred from a sequence of system inputs and observed outputs.
The same evidence characterizes unit testing as a special, one-step form of sequence testing, where the output state is more or less completely accessible to the test.
Operational model
For sequence testing, the system under test can be modeled as an input/output stepping function. For any given input and state, such a function may either fail or produce an output and a successor state. HOL-TestGen supports this style by using the state-exception monad, which models partial state-transition functions of type:
(o, σ) MONSE = σ ⇀ (o × σ)
Under this model, programs under test can be viewed as stepping functions of type:
ι ⇒ (o, σ) MONSE
where a stepping function may fail for a given state σ and input ι, or produce an output o and a successor state.
Valid test sequences in HOL-TestGen
HOL-TestGen represents valid sequence-test specifications using monadic sequencing. The evidence defines bindSE for sequential composition with value passing and unitSE for embedding a value into a computation. It then describes a valid test sequence as one in which no exception occurs and a predicate P holds for the observed outputs.
For repeated input/output steps, HOL-TestGen uses an mbind operator. Given a list of inputs:
ιs = [i1, ..., in]
mbind feeds the inputs successively into the system under test and stops when an error occurs. A valid sequence-test specification for a system under test SUT satisfying postcondition P can be expressed as:
σ |= os ← mbind ιs SUT; return (P os)
When a postcondition depends explicitly on the underlying state, the evidence uses the state-exception primitive assertSE instead of return(P).
Sequence-test scenarios
The evidence identifies two broad sequence-test scenarios:
- scenarios involving observations of the executions of local steps; and
- scenarios involving a test over the final state.
In the VAMP processor application, local steps were actions that did not report computation results, so the final-state scenario was the relevant one. The final-state check could compare conformance over the entire state, or compare only a selected part of the state, such as a value loaded into register 0.
Use in processor conformance testing
In the VAMP case study, sequence testing was used to test sequences of instructions up to a given length. The study addressed related subsets of instructions separately, including memory-related load/store operations, arithmetic operations, logic operations, and control-flow-related operations. The evidence notes that combinations of different instruction types were possible but not explored in that study.
Preconditions, also called test purposes, were added to sequence-test specifications to restrict generated instruction sequences to a desired subset. For example, a test purpose could restrict a test scenario to load and store operations by constraining the syntax of the VAMP assembly language.