Formal API specification of the PikeOS separation kernel

F. Verbeek, O. Havle, J. Schmaltz, S. Tverdyshev, H. Blasum, B. Langenstein, W. Stephan, B. Wolff, Y. Nemouchi

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

16 Citaten (Scopus)
6 Downloads (Pure)


PikeOS is an industrial operating system for safety and security critical applications in, for example, avionics and automotive contexts. A consortium of several European partners from industry and academia works on the certification of PikeOS up to at least Common Criteria EAL5+, with "+" being applying formal methods compliant up to EAL7. We have formalized the hardware independent security-relevant part of PikeOS that is to be used in a certification context. Over this model, intransitive noninterference has been proven. We present the model and the methodology used to create the model. All results have been formalized in the Isabelle/HOL theorem prover.
Originele taal-2Engels
TitelNASA Formal Methods
Subtitel7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
RedacteurenK. Havelund, G. Holzmann, R. Joshi
Plaats van productieBerlin
ISBN van elektronische versie978-3-319-17524-9
ISBN van geprinte versie978-3-319-17523-2
StatusGepubliceerd - 2015
Evenement7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA - Pasadena, CA, Verenigde Staten van Amerika
Duur: 27 apr 201529 apr 2015

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


Congres7th NASA Formal Methods Symposium (NFM 2015), April 27-29, 2015, Pasadena, CA, USA
Verkorte titelNFM 2015
Land/RegioVerenigde Staten van Amerika
StadPasadena, CA
Ander7th International Symposium on Formal Methods


Duik in de onderzoeksthema's van 'Formal API specification of the PikeOS separation kernel'. Samen vormen ze een unieke vingerafdruk.

Citeer dit