Skip to content
STIMSMITH

Test Program Generation for a Microprocessor: A Case-Study

Paper

A technical paper by Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff presenting a case study in model-based generation of microprocessor test programs. The work uses HOL-TestGen on Isabelle/HOL models of the VAMP processor to generate conformance-oriented unit and sequence tests for validating instruction-set behavior against hardware.

First seen 5/25/2026
Last seen 6/8/2026
Evidence 13 chunks
Wiki v1

WIKI

Overview

Test Program Generation for a Microprocessor: A Case-Study is a paper by Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff. It presents a case study on generating test programs from a formal microprocessor model in order to validate that a processor implements its specified instruction set correctly. The case study uses HOL-TestGen, a model-based testing environment built as an extension of Isabelle/HOL, and applies it to the VAMP processor model. [title-authors] [case-study-purpose]

The motivation is certification of critical safety and security systems. The paper states that reaching Common Criteria EAL 7 requires formal verification of specification properties as well as thorough implementation testing, including testing of the hardware platform underlying the proof architecture. [certification-context]

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

36 connections
Yakoub Nemouchi authored by → 100% 3e
The paper is authored by Yakoub Nemouchi.
Burkhart Wolff authored by → 100% 3e
The paper is authored by Burkhart Wolff.
symbolic test case generation uses → 100% 3e
The paper employs symbolic test case generation as part of its approach.
HOL-TestGen uses → 100% 3e
The paper uses HOL-TestGen as its model-based testing environment.
Isabelle/HOL uses → 100% 3e
The paper builds on an existing model developed in Isabelle/HOL and leverages its formal proofs.
black-box testing uses → 100% 3e
The paper uses black box testing concepts as part of its testing approach.
DO-178 avionics certification mentions → 100% 2e
The paper mentions DO-178 avionics certification in the context of certification kits.
unit testing uses → 100% 2e
The paper applies unit testing scenarios to test individual instructions.
Achim D. Brucker authored by → 100% 2e
The paper is authored by Achim D. Brucker.
VAMP assembler model (Isabelle/HOL) uses → 100% 2e
The paper uses the VAMP assembler model as the basis for test generation.
sequence testing uses → 100% 2e
The paper applies sequence testing to test sequences of instructions.
mbind operator uses → 100% 2e
The paper uses the mbind operator in test sequence specifications.
test program generation introduces → 100% 2e
The paper presents a case study on test program generation for a microprocessor.
hardware-in-the-loop testing uses → 100% 2e
Test programs were run against real hardware in the loop.
Abderrahmane Feliachi authored by → 100% 2e
The paper is authored by Abderrahmane Feliachi.
VAMP (Verified Architecture Microprocessor) evaluates → 90% 2e
The paper evaluates the VAMP processor's conformance to its formal model.
white-box testing uses → 95% 2e
The paper uses white box testing concepts as part of its testing approach.
model-based testing uses → 100% 2e
HOL-TestGen is described as a model-based testing environment, and the paper uses this approach.
ARM6 mentions → 85% 2e
The paper mentions ARM6 as related work with a formal processor model.
conformance testing uses → 100% 2e
The paper develops conformance test scenarios for a microprocessor.
certification kit introduces → 90% 2e
The paper proposes a model-based approach to generating certification kits.
Formal Microprocessor Model evaluates → 90% 1e
The paper evaluates the formal microprocessor model by running test programs against real hardware.
mutation testing uses → 90% 1e
The paper uses mutation testing to evaluate the quality of generated test cases.
formal verification ← compares with 85% 1e
The paper discusses how test-based approach complements formal verification.
reconfigurable model-based test program generator mentions → 85% 1e
The paper cites reconfigurable model-based test program generation as related work.
specification-driven test generation mentions → 85% 1e
The paper mentions specification-driven directed test generation as related work.
DO-254 avionics certification mentions → 100% 1e
The paper mentions DO-254 hardware certification in the context of bridging software and hardware layers.
execVAMP function uses → 100% 1e
The paper uses execVAMP as the system stepping function in test specifications.
assertSE primitive uses → 100% 1e
The paper uses assertSE to express test post-conditions.
VAMP SML executable model uses → 100% 1e
The paper uses the SML executable model to run test cases.
Springer-Verlag published by → 100% 1e
The paper was published by Springer-Verlag in the TAP 2013 proceedings.
Conformance Test Scenarios uses → 98% 1e
The paper develops conformance test scenarios to validate the microprocessor.
Formal Microprocessor Model uses → 100% 1e
The paper uses a formal model of a microprocessor to generate test programs.
Instruction Set Verification uses → 97% 1e
The test programs validate that the microprocessor implements the specified instruction set correctly.
Common Criteria EAL 7 mentions → 98% 1e
The paper mentions Common Criteria EAL 7 as a motivation for the work.
theorem proving uses → 95% 1e
The paper uses theorem proving as part of its methodology, leveraging Isabelle/HOL proofs.

LINKED ENTITIES

7 links
Achim D. Brucker AUTHORED Extracted graph relationship
Abderrahmane Feliachi AUTHORED Extracted graph relationship
Yakoub Nemouchi AUTHORED Extracted graph relationship
Burkhart Wolff AUTHORED Extracted graph relationship
HOL-TestGen APPLIES Extracted graph relationship
VAMP TARGETS Extracted graph relationship
conformance testing ADDRESSES Extracted graph relationship

CITATIONS

12 sources
12 citations — click to expand
[1] title-authors Test Program Generation for a Microprocessor: A Case Study
[2] case-study-purpose Test Program Generation for a Microprocessor: A Case Study
[3] certification-context Test Program Generation for a Microprocessor: A Case Study
[4] vamp-background Test Program Generation for a Microprocessor: A Case Study
[5] vamp-instruction-set Test Program Generation for a Microprocessor: A Case Study
[6] model-reuse Test Program Generation for a Microprocessor: A Case Study
[7] gate-to-assembly-conformance Test Program Generation for a Microprocessor: A Case Study
[8] black-box-abstraction Test Program Generation for a Microprocessor: A Case Study
[9] unit-and-sequence Test Program Generation for a Microprocessor: A Case Study
[10] instruction-groups Test Program Generation for a Microprocessor: A Case Study
[11] hol-testgen-method Test Program Generation for a Microprocessor: A Case Study
[12] unit-specification Test Program Generation for a Microprocessor: A Case Study