Better Avionics Software Reliability by Code Verification:
A Glance at Code Verification Methodology in the VerisoftXT Project

Christoph Baumann, Bernhard Beckert, Holger Blasum, Thorsten Bormer


Software reliability is a core requirement for safety- and
security-critical systems. In the area of avionics, for example, the
DO-178B standard requires extensive validation, such as software
reviews, requirement engineering, coverage analysis, and careful
design of test cases. In a broader context, EAL7 (of the Common
Criteria framework) also demands "formally verified, designed, and
tested" systems. It is part of the BMBF-supported VerisoftXT project
(www.verisoftxt.de) to explore the freedom of design offered within
these regulatory requirements, where code verification is one of the
available options.

In recent years, deductive code verification has improved to a degree
that makes it feasible for real-world programs. In the VerisoftXT
subproject Avionics, the goal is to apply formal methods to a
commercial embedded operating system. 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, i.e., when all specifications and other
required information have been added as annotations to the source code
(which is the actual user effort required), the tool verifies the code
automatically. First experiences with this new tool are described in
this paper.