25 - 27 February 2020 // Nuremberg, Germany
Formal Verification for safety-critical requirements
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.
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.
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.
Features:
- Complete mathematical analysis of production code, for finding possible requirement violation
- Automatic generation of counter examples, if a requirement can be violated
- Certified for IEC61508, ISO 26262 and related standards by TÜV SÜD
Other products from
