Verify that the C compiler correctly compiles the C code generated by SCADE Qualified Code Generator (KCG)
Esterel Technologies' Compiler Verification Kit (CVK) enables users to check that the compiler/linker correctly compiles the C code generated by KCG. This verification follows DO-178B and certification authorities guidelines (CAST-12, CAST-25).
The proof consists of verifying the compiler operation on a representative sample. The CVK contains this sample of all the elementary C code constructs and combinations of these elementary C constructs that can be generated by KCG, as well as the test vectors needed to achieve 100% MC/DC of structural code coverage. The object code generated by the cross compiler from this sample is tested as if it were manual code, including source code review and testing with structural code coverage.
Once this verification of the compiler is complete, no further low-level testing is needed on the SCADE-generated object code.
The Combined Testing Process with KCG
The use of KCG + CVK + MTC is known as Combined Testing Process and provides at least the same level of confidence on the software safety than extensive testing on C code with 100% MC/DC of structural code coverage objective.
The C Compiler Verification: Principle
- The source code generated by KCG uses a subset of C with several relevant safety properties in term of statements, data structures and control structures such as:
- " No recursion or unbounded loop
- " No code with side effects (no a += b, no side effect in function calls)
- " No functions passed as arguments
- " No arithmetic on pointers
- " No pointer on function
- " No jump statement such as "goto" or "continue"
- A test suite has been built with a set of input vectors that allows exercizing all the C constructs that can ever be generated by KCG from a SCADE model ensuring 100% MC/DC of structural code coverage
- The subset approach is accepted by safety authorities (CAST-12 §h)
- These verification activities of the C compiler are part of the overall Combined Testing Process"
CVK in the qualified process