Testing the IPC Protocol for a Real-Time Operating System

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.
Type de document :
Communication dans un congrès
7th International Conference, VSTTE 2015, San Francisco, CA,USA, Revised Selected Papers, Jul 2015, Sn Francisco, CA, USA, France. Lecture Notes in Computer Science, LNCS (9593), pp.40-59, 2015, 7th International Conference, VSTTE 2015, San Francisco, CA,USA, Revised Selected Papers. 〈10.1007/978-3-319-29613-5_3〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01274698
Contributeur : Burkhart Wolff <>
Soumis le : mardi 16 février 2016 - 10:29:55
Dernière modification le : mardi 24 avril 2018 - 13:36:15

Identifiants

Citation

Achim D. Brucker, Yakoub Nemouchi, Oto Havle, Burkhart Wolff. Testing the IPC Protocol for a Real-Time Operating System. 7th International Conference, VSTTE 2015, San Francisco, CA,USA, Revised Selected Papers, Jul 2015, Sn Francisco, CA, USA, France. Lecture Notes in Computer Science, LNCS (9593), pp.40-59, 2015, 7th International Conference, VSTTE 2015, San Francisco, CA,USA, Revised Selected Papers. 〈10.1007/978-3-319-29613-5_3〉. 〈hal-01274698〉

Partager

Métriques

Consultations de la notice

201