Test Program Generation for a Microprocessor: A Case-Study

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

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

Please cite this work as follows:
A. D. Brucker, A. Feliachi, Y. Nemouchi, and B. Wolff, “Test program generation for a microprocessor: A case-study,” in TAP 2013: Tests and proofs, L. Viganò and M. Veanes, Eds. Heidelberg: Springer-Verlag, 2013, pp. 76–95. doi: 10.1007/978-3-642-38916-0_5. Author copy: http://logicalhacking.com/publications/brucker.ea-test-program-generation-2013/

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.},
  keywords  = {Test Program Generation, Symbolic Test Case Generations,
               Black Box Testing, White Box Testing, Theorem Proving,
               Interactive Testing},
  location  = {Budapest},
  author    = {Achim D. Brucker and Abderrahmane Feliachi and Yakoub
               Nemouchi and Burkhart Wolff},
  booktitle = {{TAP} 2013: Tests And Proofs},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  number    = {7942},
  editor    = {Luca Vigan{\`o} and Margus Veanes},
  title     = {Test Program Generation for a Microprocessor: A Case-Study},
  areas     = {hardware, formal methods},
  year      = {2013},
  doi       = {10.1007/978-3-642-38916-0_5},
  pages     = {76--95},
  isbn      = {978-3-642-38915-3},
  note      = {Author copy: \url{http://logicalhacking.com/publications/brucker.ea-test-program-generation-2013/}},
}