Testing the IPC Protocol for a Real-Time Operating System

By Achim D. Brucker, Oto Havle, Yakoub Nemouchi, and Burkhart Wolff.

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.

Keywords:
Test Program Generation, Symbolic Test Case Generations, Black Box Testing, Testing Operating Systems, Certification, CC, Concurrency, Interleaving

Please cite this work as follows:
A. D. Brucker, O. Havle, Y. Nemouchi, and B. Wolff, “Testing the IPC protocol for a real-time operating system,” in Working conference on verified software: Theories, tools, and experiments, A. Gurfinkel and S. A. Seshia, Eds. Heidelberg: Springer-Verlag, 2015. doi: 10.1007/978-3-319-29613-5_3. Author copy: https://logicalhacking.com/publications/brucker.ea-ipc-testing-2015/

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.},
  keywords  = {Test Program Generation, Symbolic Test Case Generations,
               Black Box Testing, Testing Operating Systems, Certification,
               CC, Concurrency, Interleaving},
  location  = {San Francisco, California, USA},
  author    = {Achim D. Brucker and Oto Havle and Yakoub Nemouchi and
               Burkhart Wolff},
  title     = {Testing the IPC Protocol for a Real-Time Operating System},
  booktitle = {Working Conference on Verified Software: Theories, Tools, and
               Experiments},
  language  = {USenglish},
  publisher = {Springer-Verlag },
  address   = {Heidelberg },
  series    = {Lecture Notes in Computer Science },
  doi       = {10.1007/978-3-319-29613-5_3},
  isbn      = {3-540-14031-X},
  editor    = {Arie Gurfinkel and Sanjit A. Seshia},
  issn      = {0302-9743},
  areas     = {formal methods},
  year      = {2015},
  note      = {Author copy: \url{https://logicalhacking.com/publications/brucker.ea-ipc-testing-2015/}},
  pdf       = {https://logicalhacking.com/publications/brucker.ea-ipc-testing-2015/brucker.ea-ipc-testing-2015.pdf},
}