More than Testing

BTC EmbeddedValidator is a tool for formally verifying safety-critical requirements.

In modern embedded development projects, the number of possible value combinations of input signals and calibrations easily explodes towards infinity. Even with a large number of test cases, it becomes impossible to cover all potential paths through the software logic. In other words, one very important question still remains unanswered, even after rigorous testing: “Can my safety requirements be violated?”

BTC EmbeddedValidator uses model checking technology to automatically prove that a given requirement cannot be violated by your software. In other words– there is no combination of input signals and calibration values that could ever drive the system to the unsafe state we’re interested in.