QVscribe Logo

Model-Based Design Verification

Verifying that system designs implement the intended system behaviour is an increasingly difficult task. With QVtrace, rapidly query, analyze, and definitively verify the presence of expected behaviour and the absence of unwanted behaviour in complex model-based designs.

Find Faults Fast

Increase Development Efficiency

Cut Through the Noise

Get back to Engineering

Key Features

Early Detection of Design Flaws

Next-Generation Machines need Next-Generation Analysis. QVtrace harnesses the latest computational and formal mathematical methods to analyze the functional and logical structure of model-based designs, enabling engineers to definitively answer “what if ...” and “can it ever...” type questions. Empowering engineers to confidently build highly complex interconnected systems.

Document outlines with marked paragraphs
Animation of text being edited and verified as correct

Powerful and Definitive Verification

We have developed QVtrace with one goal in mind: to provide an engineering tool that easily allows for unprecedented analysis and verification of complex designs. QVtrace can detect hidden “perfect storm" scenarios or definitively verify that there are no possible states that can generate unwanted behaviour, delivering a level of confidence unmatched by standard test-case or coverage approaches.

Animation of text being edited and verified as correct

Intuitive Error Visualization

Cut through the noise by visualizing error propagation throughout the design. When QVtrace finds an error, it highlights the property that has been violated and displays a trace through the design - isolating affected components & helping you understand the implications of every design decision to avoid perfect storms scenarios.

Document outlines with marked paragraphs

The Specs

Analysis Type

Computational Formal Analysis of Model-Based Designs

Industry standard formats:

  • Simulink blocks
  • Stateflow blocks

Linear & Non-Linear Component Support

  • Trigonometric
  • Exponential
  • Logarithmic
  • Matrix arithmetic



Error Visualization Capabilities

QVtrace highlights error propagation throughout all design levels to isolate affected components, directing the engineer to the root cause of the flaw.

Counterexample Generation Capabilities

When an inconsistency between your design and your properties is detected, QVtrace generates counterexample inputs that can be used in your simulation environment to demonstrate the design flaw.

Error Visualization Capabilities

QVtrace highlights error propagation throughout all design levels to isolate affected components, directing the engineer to the root cause of the flaw.

Counterexample Generation Capabilities

When an inconsistency between your design and your properties is detected, QVtrace generates counterexample inputs that can be used in your simulation environment to demonstrate the design flaw.

An Efficient Workflow



How QVtrace Integrates into your Workflow

QVscribe Logo

Import your model-based system design

QVtrace supports Simulink model-based design components and formats

QVscribe Logo

Enter Properties to Query Design

QVtrace uses standard mathematical language to easily query design properties, similar to the Matlab language syntax.

QVscribe Logo

Analyze

If QVtrace finds an error, it generates counterexample inputs and displays visual traces for each error throughout the design. If no errors found, the design meets all specified properties for all possible input parameters, and for all time steps.

Model-Based Design Verification

QVscribe for Microsoft Word Logo

QVtrace for Simulink imports mdl and slx file formats - supporting components across multiple Simulink & Stateflow blocksets. QVtrace avoids disruption of your workflow by retaining the original Simulink visualization of your designs and generating counterexamples in Simulink-readable formats.

Now Available!

Try QVtrace

QVtrace for Aerospace & Defence


Whether it's detecting perfect storm scenarios in extremely complex systems or finding logical inconsistencies in formal specifications - our aerospace & defense partners harness the rigorous power of QVtrace for their design stage verification. Contact us to learn about deploying QVtrace in your environment

Contact Us