The power of proof for safety-critical systemsIn 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 requirementsYour 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.