Kit speeds safety critical software verification

Esterel Technologies has added the CVK (Compiler Verification Kit) to its Scade Suite development tool for safety-critical embedded software applications.

Esterel Technologies has added the CVK (Compiler Verification Kit) to its Scade Suite development tool for safety-critical embedded software applications.

Developing safety critical software implies demonstrating that the system requirements have been transformed and implemented correctly at each and every step of the software development process.

This traditionally implies time-consuming reviews and tests that generally represent more than half of a safety critical project's costs.

The Scade Suite solution enables an efficient methodology that consists of: capturing the software specifications in an unambiguous software model; verifying requirements at the model level early in the development process (when the detection and fixing of software errors are easier and cheaper); generating certifiable embedded code with the Scade KCG qualified code generator; and using Scade's new CVK, verifying the target processor with the cross-compiler environment, resulting in a proven platform for executing any volume of Scade-generated C code.

KCG, the Scade Suite automatic code generator, has been qualified as a Level A development tool under RTCA DO-178B, and certified as a product for all SIL levels under IEC61508.

Therefore KCG creates immediately certifiable code from the Scade model-based development system.

The new Compiler Verification Kit (CVK) from Esterel Technologies now enables developers to prove, with a limited effort, that the C code generated from any Scade environment will execute correctly on a selected target platform.

KCG produces an exactly defined and circumscribed subset of C.

Applied to Scade models, it generates a totally predictable C code structure.

It is therefore possible to define a reference Scade model which will produce every possible C construct on code generation that KCG can produce.

This is the foundation of Esterel's CVK.

With CVK, the user receives the following components to verify a target platform: a Scade model containing all possible Scade constructs; the reference C code generated from this model; a set of test vectors that enable testing of the C code generated from this sample model at the 100% MC/DC level (applying this test suite will ensure consistent behaviour between the Scade models running on a host development environment and the compiled Scade-generated C code running on a target); and documentation and methodology descriptions as requested by certifying bodies.

This CVK verification needs to be performed only once for any compiler/linker/processor combination, saving Scade users substantial engineering and test resources for DO-178B and IEC61508 certified projects.

CVK is processor-independent and compatible with all C cross-development systems.

"CVK provides the critical link that ensures the certifiable flow between the Scade graphical models, KCG-generated C code and object code", states Chip Downing, CEO of Esterel Technologies "Our DO-178B aerospace and defence customers, as well as our IEC61508 customers in automotive and transportation industries, will derive substantial savings and efficiencies from this exciting new Scade component".

The tools from Esterel Technologies allow the design of unambiguous specifications of software systems, to simulate them and automatically verify these designs with the help of formal methods.

Back to top