Overview

HOL-TestGen is described as a model-based testing environment that extends Isabelle/HOL. In the microprocessor case study by Brucker, Feliachi, Nemouchi, and Wolff, HOL-TestGen is used with an existing Isabelle/HOL model of a processor and operating system to synthesize conformance test programs that are run against real hardware in the loop. The approach is presented as benefiting directly from existing Isabelle/HOL models and formal proofs. [HOL-TestGen as Isabelle/HOL extension; HOL-TestGen used for hardware-in-the-loop conformance testing]

Role in model-based test generation

The cited case study uses HOL-TestGen for model-based generation of test sequences from the VAMP processor model. The authors contrast this with manually developed certification test sets: their approach reuses the design model that was already used for verification, and they identify the tight integration of verification and test environments as a distinguishing feature of HOL-TestGen. [Model-based generation from VAMP model; Verification-test integration]

In the described workflow, HOL-TestGen supports a generation pipeline with three major phases:

1. A test-case generation phase that produces a CNF-like normal form and partitions the input/output relation.
2. A test-data selection phase that uses constraint solvers, random test generation, and the integrated Z3 SMT solver to construct an instance for each partition.
3. A test-execution phase that converts instantiated test cases, called test oracles, into test-driver code run against the system under test. [HOL-TestGen generation workflow]

Sequence-test specifications and monads

Because HOL is a purely functional specification formalism and has no built-in concepts for states and state transitions, HOL-TestGen uses monads to support sequence-test specifications. The evidence identifies the state-exception monad as well suited for modeling partial state-transition functions of type (o, σ) MONSE = σ ⇀ (o × σ). [State-exception monad use]

Using this monadic representation, a program under test can be viewed as an input/output stepping function of type ι ⇒ (o, σ) MONSE: for a given state and input, the function may either fail or produce an output and successor state. The cited paper defines the usual monadic bind operation for sequential composition with value passing and unit for embedding a value into a computation. [Monadic stepping functions]

HOL-TestGen’s standard way to represent sequence test specifications uses an mbind operator over lists of inputs. The operator feeds inputs to the system under test in sequence and stops when an error occurs; valid test sequences can then be expressed as an mbind computation followed by a postcondition over the observed outputs. [Sequence-test specification with mbind]

Use in test program generation

In the cited microprocessor case study, HOL-TestGen is applied to generate test sequences from the VAMP model and to synthesize test programs for conformance scenarios. These test programs are intended to validate that a microprocessor implements the specified instruction set correctly. [HOL-TestGen used for test program generation]

The broader setting is certification-oriented testing of hardware platforms: the paper states that reaching Common Criteria EAL 7 requires both formal verification of properties on the specification and thorough testing of the implementation, including tests of the hardware platform underlying the proof architecture. [Certification motivation]