Overview

Burkhart Wolff is listed as one of the authors of the paper “Test Program Generation for a Microprocessor: A Case-Study”, alongside Achim D. Brucker, Abderrahmane Feliachi, and Yakoub Nemouchi. In the paper metadata, Wolff is associated with Univ. Paris-Sud, Laboratoire LRI, UMR8623, Orsay, France; the same author block also lists CNRS, Orsay, France, for the group of authors using LRI email addresses. [C1]

Research context in the provided evidence

The cited paper addresses test program generation for microprocessors in the context of certification of critical security or safety properties. Its abstract states that certification at higher assurance levels, including Common Criteria EAL 7, requires both formal verification of specifications and thorough implementation testing, including tests of the hardware platform used in the proof architecture. [C2]

The paper presents a case study using a formal model of a microprocessor to generate test programs. These generated programs are intended to validate that a microprocessor correctly implements its specified instruction set. [C3]

Methods and tools associated with the paper

The case study described in the paper is built on an existing model developed in Isabelle/HOL together with an operating system. The authors use HOL-TestGen, described as a model-based testing environment and an extension of Isabelle/HOL. [C4]

The work develops several conformance test scenarios in which processor models are used to synthesize test programs that are executed against real hardware in the loop. The paper states that the approach benefits directly from existing Isabelle/HOL models and formal proofs. [C5]

Publication details

The evidence identifies the work as appearing in TAP 2013, edited by M. Veanes and L. Viganò, in LNCS 7942, pages 76–95, published in 2013 by Springer-Verlag as the author’s version of the work. [C6]