datasheets.com EBN.com EDN.com EETimes.com Embedded.com PlanetAnalog.com TechOnline.com  
Events
UBM Tech
UBM Tech

Better Avionics Software Reliability by Code Verification

Authored on: Jan 1, 2009 by Christoph Baumann et al

Technical Paper

0 0
More InfoLess Info
In recent years, deductive code verification has improved to a degree that makes it feasible for realworld programs. In the VerisoftXT subproject Avionics, the goal is to apply formal methods to a commercial embedded OS. In particular, the goal is to use deductive techniques to verify functional correctness of the PikeOS microkernel. For verification, we use tools like VCC (the Verifying C Compiler) developed by Microsoft Research, which is a batch-mode verification tool. First experiences with this new tool are described in this paper.
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