Esterel Technologies>产品介绍>编译器验证工具CVK

编译器验证工具CVK

Verify that the C compiler correctly compiles the C code generated by SCADE Qualified Code Generator (KCG)

Esterel Technologies’ 编译器验证工具CVK (CVK) enables users to check that the compiler/linker introduces no discrepancy between the Source and the object code. 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 code constructs that can be generated by KCG, as well as the test vectors needed to achieve 100% MC/DC coverage. The object code generated by the cross compiler from this sample is verified as if it were manual code, including 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 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 coverage objective.

The C Compiler Verification: Principle

• The Source Code generated by KCG uses only a small subset of the C language, with a low level of complexity (defined in terms of operators such as +, -, comparisons, etc)
• A test suite has been built from all the C constructs that can ever be generated by KCG from a SCADE model, ensuring MC/DC coverage at object code level
• 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”