Verified Systems International GmbH
Quality Assurance for Embedded Systems
Quality Assurance for Embedded Systems
RTT-STO is a software analysis tool-suite that automatically performs static program analyses of C code and assembly required to receive certification credit for source-to-object code validation in the context of safety-critical avionics software.
Automatic – RTT-STO automatically performs the following program analyses, which are necessary to receive certification credit for DAL-A software:
Determine the branching structure of the assembly and match it to the original C program.
Verify correctness of memory allocation and stack frame implementations with respect to the original C program.
Detect, analyze and verify that all memory accesses in the assembly are executed as specified in the C program.
Unveil compiler-inserted function calls.
Easy-to-use – RTT-STO parses and processes unmodified programs in C and assembly, and thus does not required any intrusions to the code base.
Efficient – Analyze a large code bases with hundreds of thousands of lines of code in the order of seconds to minutes.
Supportive – RTT-STO generates spreadsheets from templates that can be provided as evidence to the certification authorities and ships with a graphical user interface that guides verification engineers through the verification workflow.
Qualified – RTT-STO comes with a tool-qualification suite for all software criticality levels according to the RTCA DO178B and DO178C standards.
Source code to object code traceability (STO) analysis is a verification activity required according to RTCA-DO178B/C for DAL-A software. There it is stated that
“additional verifications have to be performed, if the compiler generates object code that is not directly traceable to the source code statements.”
The objective of source code to object code traceability analysis is to identify all code fragments of DAL-A source code where untraceable object code exists. Untraceable code can be caused by the compiler when adding, deleting or/and morphing the assembler code, so that the one-to-one correspondence between C statements and assembler blocks implementing the C statements is broken. Untraceable branching structure in object code
For this class of untraceable object code, the compiler introduces additional decisions and associated branches that do not have any counterpart in the C-code. In principle, these branches may represent
optimisations of the original C decision structures (if, switch, while, do-while statements, so-called branch optimisation),
optimisations of sequential C statements (e.g. assignments or expression evaluations) by means of case distinctions,
compiler-generated built-in error detection, and
compiler-generated checks.
Compilers may also introduce sequential instructions that are not traceable to the C code, while the branching structures on C and assembler level are equivalent. These situations can be classified as follows.
Instructions for function initialisation, e.g., local variable setup on the stack.
Calls to “hidden” library routines, performing, for example, arithmetic operations.
Finally, the compiler may re-arrange the object code for optimisation purposes, such that the one-to-one correspondence between C statements and sequential object code blocks implementing these statements is broken. Morphed code may arise from the following types of optimisations.
Effects of instruction scheduling: move/load/store/branch operations may be re-grouped by the compiler in order to optimise the parallelisation options offered by the RISC processor. As a consequence, the one-to-one correspondence between C-statements and sequential assembler blocks is broken: some move operations, for example, located in the assembler block associated with C statement 1 may be needed to implement C statement 2.
Effects of register tracking: the compiler tracks the contents of registers to avoid reloading values if they are used again soon. Variables, constants, and structure references such as (a.b) are tracked through linear C code blocks. Again, this has the effect that the one-to-one correspondence between C-statements and sequential assembler blocks is broken: move operations loading values into registers may be missing in the assembler block associated with one C statement, if the required value has already been stored in the register at an earlier point in time.
STO analysis helps to verify the consistency between C code and assembler code, so that compilers may be used that have not been validated. Therefore it is an explicit objective of the STO analysis to reveal object code that has been created due to compiler errors, and not just for optimisation purposes or other justified technical reasons as the ones described in the paragraphs above. Erroneous compilers may introduce, for example,
illegal sizes of memory chunks allocated for variables of a given type (that is, errors in the implementation of the variable type model),
illegal branching instructions,
load/store operations with illegal source/target addresses,
register move operations with illegal source/target registers,
Points 2 – 4 may lead to writes at illegal destination addresses. These writes would not necessarily be detected during testing activities, since there the correctness of the expected outputs are checked, but the absence of illegal writes to arbitrary memory addresses can usually not be comprehensively verified during testing.
Announcements on new RTT-STO releases are available via
RSS feed 
.
This feed is also used to inform about any serious problems with some
released versions.
A complete list of all RTT-STO related announcements is available here.