The power of proof for safety-critical systems

In model-based development there are always areas that require 100 % safety. For example when it comes to meeting the strict requirements of ISO 26262 and IEC 61508 - here, it is essential to check the model and code meticulously. To ensure that safety-relevant systems no longer leave any room for doubt, we have developed a tool that delivers 100 % mathematical proof:
BTC EmbeddedValidator for formal verification of TargetLink models. Set new quality standards in the model-based testing process and enjoy the benefits of the best foundation for creative engineering.

Why not get this verified as soon as possible?

BTC EmbeddedValidator provides outstanding opportunities to formally verify your TargetLink model:

• Formal requirements specification
• Formal model verification
• Generation of counterexamples
• Automatic debugging support
• Fully automated robustness analysis of the models
• Location of unreachable model components
• User-defined reachability analysis
• Provides verification support regarding the strict requirements of ISO 26262 und IEC 61508
• Seamless TargetLink integration
• Comprehensive reporting of results

Does your model deliver on its promises?

As an engineer, you know best of all that even the smallest errors can have far-reaching consequences. That’s why BTC EmbeddedValidator supports many use-cases that allow you to conduct a conclusive quality check on your model.

Formal model verification against requirements

Your proof of validity of all functional and safety-relevant requirements of a model:
Using the TargetLink API, BTC EmbeddedValidator can extract a precise mathematical representation of a TargetLink model and formally verify it using model checking.

More opportunities to be creative

Robustness analysis of the model

• Range Violation Analysis

Could there be a scenario in which an overflow or underflow for a certain variable occurs? The range violation analysis will reveal this.

• Drive to State

Choose between one, several or all the states of a Stateflow Chart when you perform a reachability analysis in one verification task.

• Drive to Configuration

An extension of the Drive to State analysis that informs you whether two or more states in different parallel sub-charts are reachable at the same time.

Drive to Property

Check whether a model state is reachable in which a specific property holds. In addition all available variables and states of the selected Stateflow chart or subsystem are shown, so that a Boolean expression can be created for the relevant property.

Failure Analysis Support

An integrated Waveform Diagram providing a quick overview of the analysis results is one component of BTC EmbeddedValidator. Another is the automatic support of the Simulink simulation: if BTC EmbeddedValidator generates a counterexample, an M-Script is automatically generated for the Simulink simulator, which can then be started together with the model at the touch of a button.

Report Generation

Along with general details about the users, dates and model environments, a report is also generated with full information on the profile of the defined analyses and proofs. In HTML, TXT or XML as required.

 Booklet BTC EmbeddedValidator