Skip to content
MathWorks - Mobile View
  • MathWorks 계정에 로그인합니다.MathWorks 계정에 로그인합니다.
  • Access your MathWorks Account
    • 내 계정
    • 나의 커뮤니티 프로필
    • 라이선스를 계정에 연결
    • 로그아웃
  • 제품
  • 솔루션
  • 아카데미아
  • 지원
  • 커뮤니티
  • 이벤트
  • MATLAB 받기
MathWorks
  • 제품
  • 솔루션
  • 아카데미아
  • 지원
  • 커뮤니티
  • 이벤트
  • MATLAB 받기
  • MathWorks 계정에 로그인합니다.MathWorks 계정에 로그인합니다.
  • Access your MathWorks Account
    • 내 계정
    • 나의 커뮤니티 프로필
    • 라이선스를 계정에 연결
    • 로그아웃

비디오 및 웨비나

  • MathWorks
  • 비디오
  • 비디오 홈
  • 검색
  • 비디오 홈
  • 검색
  • 영업 담당 문의
  • 평가판 신청
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

  • 영업 담당 문의
  • 평가판 신청

MathWorks

Accelerating the pace of engineering and science

MathWorks는 엔지니어와 과학자들을 위한 테크니컬 컴퓨팅 소프트웨어 분야의 선도적인 개발업체입니다.

활용 분야 …

제품 소개

  • MATLAB
  • Simulink
  • 학생용 소프트웨어
  • 하드웨어 지원
  • File Exchange

다운로드 및 구매

  • 다운로드
  • 평가판 신청
  • 영업 상담
  • 가격 및 라이선스
  • MathWorks 스토어

사용 방법

  • 문서
  • 튜토리얼
  • 예제
  • 비디오 및 웨비나
  • 교육

지원

  • 설치 도움말
  • MATLAB Answers
  • 컨설팅
  • 라이선스 센터
  • 지원 문의

회사 정보

  • 채용
  • 뉴스 룸
  • 사회적 미션
  • 고객 사례
  • 회사 정보
  • Select a Web Site United States
  • 신뢰 센터
  • 등록 상표
  • 정보 취급 방침
  • 불법 복제 방지
  • 애플리케이션 상태
  • 매스웍스코리아 유한회사
  • 주소: 서울시 강남구 삼성동 테헤란로 521 파르나스타워 14층
  • 전화번호: 02-6006-5100
  • 대표자 : 이종민
  • 사업자 등록번호 : 120-86-60062

© 1994-2022 The MathWorks, Inc.

  • Naver
  • Facebook
  • Twitter
  • YouTube
  • LinkedIn
  • RSS

대화에 참여하기