The power of proof for safety-critical systems
BTC EmbeddedValidator is a tool for the formal verification of safety-critical requirements. Formal verification is performed on production C-code and takes formalized requirements from BTC EmbeddedSpecifier as a starting point.
More than Testing
The number of possible value combinations for input signals and calibration values is almost infinite for a typical software component in modern embedded development projects. It is therefore obvious that even a large number of test cases can never cover all possible paths through the component. This means that even with a good set of test cases, there is still one question which remains unanswered: “Can a particular safety requirement be violated?”
BTC EmbeddedValidator uses Model-Checking technology to automatically provide complete mathematical proof that shows a requirement cannot be violated by the analyzed system. This guarantees that there is no combination of input signals and calibration values that would drive the system to a state in which the requirement is violated.
Generation of counter examples
In case a requirement can be violated, BTC EmbeddedValidator provides a counter example in the form of a test case. This generated test shows an example of how to drive the system into a state where the corresponding requirement is violated.
In case a counter example has been generated, you can use the powerful debugging capabilities of BTC EmbeddedPlatform to automatically generate a debug environment. This can either be done as a Simulink/TargetLink model or as a Microsoft Visual Studio project.