Testing the IPC Protocol for a Real-Time Operating System

Achim D. Brucker, Oto Havle, Yakoub Nemouchi und Burkhart Wolff

Cover for brucker.ea:ipc-testing:2015.In this paper, we adapt model-based testing techniques to concurrent code, namely for test generations of an (industrial) OS kernel called PikeOS@. Since our data-models are complex, the problem is out of reach of conventional model-checking techniques. Our solution is based on symbolic execution implemented inside the interactive theorem proving environment Isabelle/HOL extended by a plugin with test generation facilities called HOL-TestGen.

As a foundation for our symbolic computing techniques, we refine the theory of monads to embed interleaving executions with abort, synchronization, and shared memory to a general but still optimized behavioral test framework.

This framework is instantiated by a model of PikeOS inter-process communication system-calls. Inheriting a micro-architecture going back to the L4 kernel, the system calls of the IPC-API are internally structured by atomic actions; according to a security model, these actions can fail and must produce error-codes. Thus, our tests reveal errors in the enforcement of the security model.

Schlüsselwörter: test program generation, symbolic test case generations, black box testing, testing operating systems, certification, CC, concurrency, interleaving
Kategorien:
Dokumente: (Artikel als PDF Datei)

QR Code for brucker.ea:ipc-testing:2015.Bitte zitieren sie diesen Artikel wie folgt:
Achim D. Brucker, Oto Havle, Yakoub Nemouchi und Burkhart Wolff. Testing the IPC Protocol for a Real-Time Operating System. In Working Conference on Verified Software: Theories, Tools, and Experiments. Lecture Notes in Computer Science, Springer-Verlag, 2015.
Schlüsselwörter: test program generation, symbolic test case generations, black box testing, testing operating systems, certification, CC, concurrency, interleaving
(Artikel als PDF Datei) (BibTeX) (Endnote) (RIS) (Word) (doi:10.1007/978-3-319-29613-5_3) (Share article on LinkedIn. Share article on CiteULike.)

BibTeX
@InCollection{ brucker.ea:ipc-testing:2015,
abstract = {In this paper, we adapt model-based testing techniques to concurrent code, namely for test generations of an (industrial) OS kernel called PikeOS\@. Since our data-models are complex, the problem is out of reach of conventional model-checking techniques. Our solution is based on symbolic execution implemented inside the interactive theorem proving environment Isabelle/HOL extended by a plugin with test generation facilities called HOL-TestGen.\\\\As a foundation for our symbolic computing techniques, we refine the theory of monads to embed interleaving executions with abort, synchronization, and shared memory to a general but still optimized behavioral test framework.\\\\This framework is instantiated by a model of PikeOS inter-process communication system-calls. Inheriting a micro-architecture going back to the L4 kernel, the system calls of the IPC-API are internally structured by atomic actions; according to a security model, these actions can fail and must produce error-codes. Thus, our tests reveal errors in the enforcement of the security model.},
address = {Heidelberg},
author = {Achim D. Brucker and Oto Havle and Yakoub Nemouchi and Burkhart Wolff},
booktitle = {Working Conference on Verified Software: Theories, Tools, and Experiments},
doi = {10.1007/978-3-319-29613-5_3},
editor = {Arie Gurfinkel and Sanjit A. Seshia},
isbn = {3-540-14031-X},
issn = {0302-9743},
keywords = {test program generation, symbolic test case generations, black box testing, testing operating systems, certification, CC, concurrency, interleaving},
language = {USenglish},
location = {San Francisco, California, USA},
pdf = {https://www.brucker.ch/bibliography/download/2015/brucker.ea-ipc-testing-2015.pdf},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
title = {Testing the IPC Protocol for a Real-Time Operating System},
url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-ipc-testing-2015},
year = {2015},
}