/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 73
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 78
" /> /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96

Warning: Attempt to read property "value" on null in /tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php on line 96
"/> KIT - Application-oriented Formal Verification - <br /> <b>Warning</b>: Undefined array key "title" in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br /> <br /> <b>Warning</b>: Attempt to read property "value" on null in <b>/tmp/8691dd922c688b39445d8134f863fc050c4898b2_0.file.basen.html.php</b> on line <b>99</b><br />
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.