loader image

Test Solutions for Model-based Development

How can I create the needed millions of scenarios?

How can I avoid the test explosion problem?

How can I find out if my tests are passed or failed?

BTC EmbeddedPlatform

Formal Verification Package

The power of proof for safety-critical softwares

INTRODUCTION

Formal Verification Package

Formal Verification Package provides feature set 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 EmbeddedPlatform 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.

SUPPORTED FEATURES

  • Formal Verification with Model Checking
    incl. Mathematically complete proof showing absence of requirement violation
    incl. Counter-example generation
  • MIL/SIL Debug Environment Export
  • Formal Specification with Universal Pattern
  • MATLAB-APIs, REST-APIs
Play now
Play Video
Play now
Play Video

FORMAL VERIFICATION PACKAGE

Use Cases

Formal Verification

The power of proof for safety-critical systems

Formal Specification

Intuitive formal specification of safety requirements

FORMAL VERIFICATION PACKAGE

Verification Targets

dSPACE TargetLink

Static analysis of Model behavior
Static analysis of C-Code behavior

Mathworks Embedded Coder

Static analysis of C-Code behavior

C-Code

Static analysis of C-Code behavior

ADD-ON

RTT-Observer Generator​

RTT-Observer technology has been developed by BTC Embedded Systems and dSPACE. The technology enables enhancement of dSPACE VEOS and HIL Test by real time Formal Test.

This addon exports “watchdogs” so-called RTT-Observers (Real Time Testing Observer) out of existing Formal Requirements. Each Requirement Observer keeps watching dSPACE HIL/VEOS simulation and reports whether the corresponding Formal Requirement is fulfilled or not in real time.

Due to the parallel execution of the RTT-Observers and dSPACE HIL system/VEOS, the test effort remains mostly unchanged whereas the test depth dramatically increases based on the continuous validation of all tests against all requirements. Moreover, the high degree of integration into dSPACE products like ControlDesk Next Generation and AutomationDesk enables a comfortable and efficient way of using requirement observers in different projects.

NOTE: dSPACE Real Time Testing (RTT) Observer Library is required for the solution.

Read more on www.dspace.com

certified

ISO 26262

BTC EmbeddedPlatform has been certified by German TÜV SÜD as fit for usage in safety critical software development projects.

The certificate addresses different standards including IEC 61508-3:3010, ISO 26262, EN 50128, IEC 62304 as well as ISO 25119.

For the automotive standard ISO 26262, we have been certified with the highest tool confidence level TCL and the certificate is valid for all ASIL levels including ASIL D.

We provide the certificate and the corresponding report to our customers free of charge upon request, which almost eliminates any effort for tool qualification measures on the customer side.

Request an Evaluation License

If you would like to try out our tools, we will gladly provide an evaluation license free of chargeEvaluations include a free launch workshop and also provide an opportunity for you to meet one-on-one with our support and engineering teams.

Schedule a Meeting with our Engineering Team

Do you have any questions or want to see our tools in action? If so, please use the link below to schedule a meeting, where a member of our engineering team will be happy to show you the features and use cases and directly answer any questions you might have.

Request an Evaluation License​

If you would like to try out our tools, we will gladly provide an evaluation license free of chargeEvaluations include a free launch workshop and also provide an opportunity for you to meet one-on-one with our support and engineering teams.

Schedule a Meeting with our Engineering Team

Do you have any questions or want to see our tools in action? If so, please use the link below to schedule a meeting, where a member of our engineering team will be happy to show you the features and use cases and directly answer any questions you might have.

BTC EMBEDDED SYSTEMS BLOG

From our Blog​

Sharing insights on embedded software development, model-based design, automatic code generation and ISO 26262 compliant testing.

PRODUCT VIDEOS

Videos

Discover some of the main features of our products in these short videos.

Formal Test Package

Highly automated and advanced requirements-based testing enhanced by formal methods and automatic test generation