Skip to content
MathWorks - Mobile View
  • Inicie sesión cuenta de MathWorksInicie sesión cuenta de MathWorks
  • Access your MathWorks Account
    • Mi Cuenta
    • Mi perfil de la comunidad
    • Asociar Licencia
    • Cerrar sesión
  • Productos
  • Soluciones
  • Educación
  • Soporte
  • Comunidad
  • Eventos
  • Obtenga MATLAB
MathWorks
  • Productos
  • Soluciones
  • Educación
  • Soporte
  • Comunidad
  • Eventos
  • Obtenga MATLAB
  • Inicie sesión cuenta de MathWorksInicie sesión cuenta de MathWorks
  • Access your MathWorks Account
    • Mi Cuenta
    • Mi perfil de la comunidad
    • Asociar Licencia
    • Cerrar sesión

Vídeos y webinars

  • MathWorks
  • Vídeos
  • Vídeos-Inicio
  • Buscar
  • Vídeos-Inicio
  • Buscar
  • Comuníquese con ventas
  • Software de prueba
6:33 Video length is 6:33.
  • Description
  • Full Transcript
  • Related Resources

How to Debug a Property Proving Counterexample

Property proving with Simulink Design Verifier™ is a static analysis technique that uses formal methods to prove whether a given property will always be valid. This technique can help you formally verify that specific requirements implemented in your design will always be met. If a property is invalidated, a counterexample will be automatically generated for debugging.

Learn how to perform property proving with Simulink Design Verifier and see how to debug an automatically generated counterexample with the Model Slicer tool from Simulink Check™.

Some requirements are difficult to verify completely through simulation-based tests.

Let’s use four requirements for a simplified airplane thrust reverser system to demonstrate. Thrust reversers are used to slow the airplane down on the runway after landing.

We need to make sure that the thrust reversers are not deployed during certain unsafe conditions. Therefore, there are four safety requirements which define when to prohibit thrust reverser deployment.

Notice the use of “shall not” in each requirement? The use of “shall not” in a requirement may indicate that the requirement is difficult to verify completely. How can you be sure you have accounted for unusual conditions?

With simulation-based testing, we would need to create many, many test cases to accomplish this goal, if that is even possible!

This is where property proving can help.

Property proving with Simulink Design Verifier is a static analysis technique that uses formal methods to prove whether a given property will always be valid. This technique can help you formally verify that specific requirements implemented in your design will always be met.

This video will walk you through an example which shows you how to use Simulink Design Verifier and the Model Slicer feature in Simulink Check to formally verify these four thrust reverser safety requirements and debug an automatically generated counterexample.

This Simulink model contains logic defined in a Stateflow state chart to determine when to deploy thrust reversers after the airplane has landed.

Four properties have been defined to verify the safety requirements; one property per requirement. The properties have been defined in a Verification Subsystem, which does not generate code. Properties can be defined using Simulink blocks, Stateflow state charts, or MATLAB code in a MATLAB Function Block.

Let’s look at the Weight-on-Wheels requirement’s property as an example. The Weight-on-Wheels, or “WOW”, sensors are used to determine when the airplane is on the ground.

The property description for the WOW safety requirement is shown as an Annotation in the Verification Subsystem: “If two WOW sensors are false, deploy cannot be true.” In other words, if the airplane is in the air, the thrust reversers should not be deployed.

The WOW property definition uses an Implies block from the Simulink Design Verifier library. The Implies block lets you specify a condition to produce a given response. The Assertion block from the Simulink Model Verification library is also used, which lets Simulink Design Verifier know that a property has been defined.

Let’s run Simulink Design Verifier in Property Proving Mode to verify that all four of the safety requirements are being met by the design.

Simulink Design Verifier was able to invalidate three of the four properties.

A counterexample test vector for each property violation has been automatically generated for debugging.

Counterexamples can be difficult to debug because Simulink Design Verifier will try to find a violation in as few time steps as possible, and the tool does not have any knowledge of what is physically realistic in your overall system.

You need to provide the engineering insight. One way to do this is to use Proof Assumptions to limit a signal’s range, rate of change, or other characteristics. Simulink Design Verifier will use these assumptions when analyzing the model.

We don’t want to add assumptions quite yet as to not rule anything out.

Instead, let’s use Model Slicer from Simulink Check to debug a counterexample. Let’s start with the WOW property.

This is as simple as selecting the Assertion block in the WOW property subsystem, then clicking “Debug” in the Design Verifier results window.

Model Slicer is automatically set up to help us step through the counterexample for the WOW property.

Model Slicer allows you to step through a simulation to see which parts of a model are active and what the signal values are during any step within a simulation.

If we step back and then forward through the short counterexample simulation, we can see that there is a specific transient condition wherein a sudden change in the airspeed and wheel speed sensor values can violate the WOW requirement. This is an unusual scenario but represents the type of condition which would be difficult to define in a simulation-based test.

After analyzing the counterexamples for the other properties, and by using my own engineering experience designing similar logic, I can see that the design does not adequately account for sudden changes in signal values after landing.

There are many ways we could address this. I’ve decided to add a new requirement which will add a short delay to enable thrust reverser deployment after the appropriate conditions are met. This short delay will not affect the physical performance of the thrust reversers.

Let’s open the fixed model and run property proving again.

All set!

This example showed how to use Simulink Design Verifier and Model Slicer from Simulink Check to use property proving to analyze safety requirements and debug a counterexample.

You can also link proof objectives to requirements in Requirements Toolbox to manage verification results for property proving in addition to simulation-based tests.

Visit the Simulink Design Verifier product page or the Simulink Check product page to request a trial.

Related Products

  • Simulink Design Verifier
  • Simulink Check

3 Ways to Speed Up Model Predictive Controllers

Read white paper

A Practical Guide to Deep Learning: From Data to Deployment

Read ebook

Bridging Wireless Communications Design and Testing with MATLAB

Read white paper

Deep Learning and Traditional Machine Learning: Choosing the Right Approach

Read ebook

Hardware-in-the-Loop Testing for Power Electronics Control Design

Read white paper

Predictive Maintenance with MATLAB

Read ebook

Electric Vehicle Modeling and Simulation - Architecture to Deployment : Webinar Series

Register for Free

How much do you know about power conversion control?

Start quiz
Related Information
Related Information
Try the example

Feedback

Featured Product

Simulink Design Verifier

  • Request Trial
  • Get Pricing

Up Next:

54:54
Model-Based Design for DO-178C Software Development with...

Related Videos:

2:57
Using 'dbstop If Error' and Conditional Breakpoints to...
3:51
Protecting Intellectual Property in Subsystems
42:25
Model-Based Design for DO-178C Software Development with...
4:15
How to Label a Series of Points on a Plot in MATLAB

View more related videos

MathWorks - Domain Selector

Select a Web Site

Choose a web site to get translated content where available and see local events and offers. Based on your location, we recommend that you select: .

  • Switzerland (English)
  • Switzerland (Deutsch)
  • Switzerland (Français)
  • 中国 (简体中文)
  • 中国 (English)

You can also select a web site from the following list:

How to Get Best Site Performance

Select the China site (in Chinese or English) for best site performance. Other MathWorks country sites are not optimized for visits from your location.

Americas

  • América Latina (Español)
  • Canada (English)
  • United States (English)

Europe

  • Belgium (English)
  • Denmark (English)
  • Deutschland (Deutsch)
  • España (Español)
  • Finland (English)
  • France (Français)
  • Ireland (English)
  • Italia (Italiano)
  • Luxembourg (English)
  • Netherlands (English)
  • Norway (English)
  • Österreich (Deutsch)
  • Portugal (English)
  • Sweden (English)
  • Switzerland
    • Deutsch
    • English
    • Français
  • United Kingdom (English)

Asia Pacific

  • Australia (English)
  • India (English)
  • New Zealand (English)
  • 中国
    • 简体中文Chinese
    • English
  • 日本Japanese (日本語)
  • 한국Korean (한국어)

Contact your local office

  • Comuníquese con ventas
  • Software de prueba

MathWorks

Accelerating the pace of engineering and science

MathWorks es el líder en el desarrollo de software de cálculo matemático para ingenieros

Descubra…

Explorar productos

  • MATLAB
  • Simulink
  • Software para estudiantes
  • Soporte para hardware
  • File Exchange

Probar o comprar

  • Descargas
  • Software de prueba
  • Comuníquese con ventas
  • Precios y licencias
  • Cómo comprar

Aprender a utilizar

  • Documentación
  • Tutoriales
  • Ejemplos
  • Vídeos y webinars
  • Formación

Obtener soporte

  • Ayuda para la instalación
  • MATLAB Answers
  • Consultoría
  • Centro de licencias
  • Comuníquese con soporte

Acerca de MathWorks

  • Ofertas de empleo
  • Sala de prensa
  • Misión social
  • Casos prácticos
  • Acerca de MathWorks
  • Select a Web Site United States
  • Centro de confianza
  • Marcas comerciales
  • Política de privacidad
  • Antipiratería
  • Estado de las aplicaciones

© 1994-2022 The MathWorks, Inc.

  • Facebook
  • Twitter
  • Instagram
  • YouTube
  • LinkedIn
  • RSS

Únase a la conversación