Overview

Model-based test case generation is an approach in which a model of the system under test is used as the basis for producing test cases or test programs. In the VAMP microprocessor case study, a formal processor model developed in Isabelle/HOL was adapted and reused to generate test cases for checking whether hardware conforms to the VAMP processor model. The generated tests validate that a microprocessor implements the specified instruction set correctly.

Role in certification-oriented testing

The case study frames model-based generation as useful for certification contexts where both formal verification and thorough implementation testing are required. For high assurance levels such as Common Criteria EAL 7, the paper states that properties must be formally verified on the specification and the implementation must be tested thoroughly, including tests of the underlying hardware platform. The generated test programs are described as the basis for a certification kit, i.e., a set of test cases that vendors may provide to support customer certification processes.

Model reuse and HOL-TestGen

A key feature of the described approach is that it reuses a design or verification model rather than developing certification test sets manually. The authors contrast their method with the usual separation between specification-level verification and test-set development, noting that certification-kit test sets are often manually developed. Their model-based approach uses the design model already used for verification, and specifically uses HOL-TestGen to generate test sequences from the VAMP model. Because HOL-TestGen is built on top of Isabelle/HOL and test specifications are expressed in higher-order logic, the approach can directly benefit from existing verification models.

Black-box and conformance setting

The cited work describes a black-box testing scenario in which an abstract description of the system under test is used as the basis for test generation. In the VAMP case, the processor model is used to extract abstract test cases, with the goal of checking that the processor behaves as described by the assembler model independently of internal implementation details such as interrupt handling, virtual memory, caching, pipelining, and instruction reordering.

Test specifications and generated cases

For unit instruction testing, the evidence describes a test specification based on preconditions and postconditions over inputs and results. Each generated test case consists of an instruction, an initial configuration, and the resulting configuration after executing the instruction. The paper states that HOL-TestGen produces tests for all possible instructions from such a specification, while subsets of instructions can be isolated by adding a precondition that specifies the instruction type.

Unit and sequence testing

The case study applies two model-based scenarios: unit testing and sequence testing. Unit testing tests individual operations or instructions with different data and assumes control over the initial state as well as access to internal states after the test. Sequence testing is used for instruction sequences up to a given length and infers test results from sequences of system inputs and observed outputs. In the study, instruction subsets included memory-related load and store operations, arithmetic operations, logic operations, and control-flow operations.

Relationship to conformance testing

The generated tests are used for conformance checking: a system-under-test state is compared with the model-controlled state using a conformance relation. In the unit-test specification shown in the paper, the system under test is compared with execution of the model instruction, with an executable equality comparing registers and a bounded portion of memory. This positions model-based test case generation as an approach that applies to conformance testing when the test objective is to determine whether an implementation behaves according to its model.