datasheets.com EBN.com EDN.com EETimes.com Embedded.com PlanetAnalog.com TechOnline.com  
Events
UBM Tech
UBM Tech
Welcome Guest Log In | Register | Benefits

Proving Memory Separation in a Microkernel by Code Level Verification

Authored on: May 1, 2011 by Christoph Baumann et al

Technical Paper

0 0
More InfoLess Info
Often, an integrated mixed-criticality system is built in an environment which provides separation functionality for available on-board resources. In this paper we treat such an environment: the PikeOS separation kernel—a commercial real-time embedded operating system. PikeOS allows applications with different safety and security levels to run on the same hardware. Obviously, a mixed-criticality system built on PikeOS relies on the correct implementation of the separation mechanisms. In the context of the Verisoft XT and TECOM projects we apply deductive formal software verification to the PikeOS separation mechanisms in order to validate this security requirement.
0 comments
write a comment

Please Login

You will be redirected to the login page

×

Please Login

You will be redirected to the login page

×

Please Login

You will be redirected to the login page