pdfreaders.org

Test Program Generation for a Microprocessor: A Case-Study

by Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff

Cover for brucker.ea:test-program-generation:2013.Certifications demonstrating that certain security or safety requirements are met by a system are becoming increasingly important for a wide range of products. Certifying large systems like operating systems up to Common Criteria EAL 4 is common practice today, and higher certification levels are at the brink of becoming reality.

To reach EAL 7 one has to formally verify properties on the specification as well as test the implementation thoroughly. In this paper, we present a case study that uses a formal model of a microprocessor for generat- ing test programs. These test programs validate that a microprocessor implements the specified instruction set correctly.

We built our case study on an existing model that was, together with an operating system, developed in Isabelle/HOL. We use HOL-TestGen, a model-based testing environment which is an extension of Isabelle/HOL. We develop a number of conformance test scenarios, where processor models were used to synthesize test programs that were run against real hardware in the loop. Our test case generation approach directly benefits from the existing models and formal proofs in Isabelle/HOL.

Keywords: test program generation, symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
Categories: ,
Documents: (full text as PDF file)

QR Code for brucker.ea:test-program-generation:2013.Please cite this article as follows:
Achim D. Brucker, Abderrahmane Feliachi, Yakoub Nemouchi, and Burkhart Wolff. Test Program Generation for a Microprocessor: A Case-Study. In TAP 2013: Tests And Proofs. Lecture Notes in Computer Science (7942), pages 76-95, Springer-Verlag, 2013.
Keywords: test program generation, symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing
(full text as PDF file) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-642-38916-0_5) (Share article on LinkedIn. Share article on CiteULike. )

BibTeX
@InCollection{ brucker.ea:test-program-generation:2013,
abstract = {Certifications demonstrating that certain security or safety requirements are met by a system are becoming increasingly important for a wide range of products. Certifying large systems like operating systems up to Common Criteria EAL 4 is common practice today, and higher certification levels are at the brink of becoming reality.\\\\To reach EAL 7 one has to formally verify properties on the specification as well as test the implementation thoroughly. In this paper, we present a case study that uses a formal model of a microprocessor for generat- ing test programs. These test programs validate that a microprocessor implements the specified instruction set correctly.\\\\We built our case study on an existing model that was, together with an operating system, developed in Isabelle/HOL. We use HOL-TestGen, a model-based testing environment which is an extension of Isabelle/HOL. We develop a number of conformance test scenarios, where processor models were used to synthesize test programs that were run against real hardware in the loop. Our test case generation approach directly benefits from the existing models and formal proofs in Isabelle/HOL.},
address = {Heidelberg},
author = {Achim D. Brucker and Abderrahmane Feliachi and Yakoub Nemouchi and Burkhart Wolff},
booktitle = {{TAP} 2013: Tests And Proofs},
doi = {10.1007/978-3-642-38916-0_5},
editor = {Luca Vigan{\`o} and Margus Veanes},
isbn = {978-3-642-38915-3},
keywords = {test program generation, symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing},
language = {USenglish},
location = {Budapest},
number = {7942},
pages = {76--95},
pdf = {https://www.brucker.ch/bibliography/download/2013/brucker.ea-test-program-generation-2013.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Test Program Generation for a Microprocessor: A Case-Study},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-test-program-generation-2013},
year = {2013},
}