Simulink Design Verifier

설계 오류를 식별하고, 요구 사항 준수를 증명하고 테스트를 생성하기

Simulink Design Verifier™는 Formal method를 사용하여 모델에 숨겨진 설계 오류를 식별합니다. Simulink Design Verifier는 모델에서 정수 오버플로, 데드 로직, 배열 액세스 위반 및 0으로 나누기를 일으킬 수 있는블록을 탐지합니다. Simulink Design Verifier는 설계가 기능적 요구 사항을 충족하는지 Formal method로 검증할 수 있습니다. 각각의 설계 오류 또는 요구 사항 위반에 대한 디버깅용 시뮬레이션 테스트 케이스를 생성합니다.

Simulink Design Verifier는 기존의 요구 사항 기반 테스트 케이스를 확장하기 위해 모델 커버리지와 사용자 지정 objective를 만족하기 위한 테스트 케이스를 생성합니다. 이러한 테스트 케이스를 활용하여 Condition, Decision, MCDC 및 사용자 지정 커버리지 Objective들을 만족하는 모델을 만들 수 있습니다. 커버리지 목표 외에도 사용자 지정 테스트 목표를 정하여 요구 사항 기반 테스트 objective 를 자동으로 생성할 수 있습니다.

IEC Certification Kit (for ISO 26262 and IEC 61508) 및 DO Qualification Kit (for DO-178 and DO-254)를 통해 업계 표준을 지원합니다.

시작하기:

설계 오류 탐지

런타임 오류, 진단 오류 및 데드 로직을 포함하여 시뮬레이션 전에 모델의 설계 오류를 발견합니다.

런타임 오류와 진단 오류

시뮬레이션을 실행하기 전에 정수 오버플로, 0으로 나누기, 배열 범위를 벗어남, 비정규 값 및 부동 소수점 오류는 물론 데이터 유효성 오류를 포함하여 런타임 오류와 모델링 오류를 탐지할 수 있습니다. 

데드 로직

시뮬레이션과 생성된 코드의 실행 중에 동작되지 않는 객체를 모델에서 찾습니다.

모델에서 데드 로직 보기.

테스트 케이스 생성

구조와 기능적 커버리지 목표를 달성하기 위해 동적 시뮬레이션용 테스트 케이스를 생성합니다.

커버리지를 늘확장하기한 테스트 케이스

불완전한 모델 커버리지를 위해 수동으로 만든 기존 테스트 케이스를 확장합니다.

요구 사항 기반 테스트 케이스

모델의 시스템 요구사항으로부터 테스트 케이스를 생성합니다.

C/C++ 코드용 테스트 케이스

StateflowSimulink에서 호출되거나 생성된 코드의 커버리지를 향상시키기 위해 테스트 케이스를 생성합니다.

C 코드를 호출하는 모델용 테스트 생성하기.

요구 사항 기반 검증

MATLAB, Simulink 및 Stateflow를 사용하여 표현된 정형 요구 사항을 검증할 수 있습니다.

안전 요구 사항

MATLAB®, Simulink 및 Stateflow를 사용하여 정형화 된 안전 요구 사항에 따라 설계가 동작하는지 검증합니다.

Variant Model 의 간소화

Variant Reducer를 사용하여 유효한 구성의 서브셋용 축소 모델을 생성합니다.

배포를 위해 모델 간소화하기

Master Variant 모델을 완벽히 검증한 후 Variant Reducer를 사용하여 유효한 구성의 서브셋의 축소된 모델을 생성합니다. 모든 관련 파일과 variable dependency도 감소합니다. 축소된 아티팩트는 별도의 폴더에 패키징되어 있어 고객과 파트너사와 쉽게 배포하고 공유할 수 있습니다.

축소 모델 만들기.

최신 기능

System Object의 오류 감지

Simulink에서 System Object를 사용하여 MATLAB 코드의 오류를 감지하고, 테스트를 생성하며 속성을 검증

HISM(High-Integrity System Modeling) 지침 위반 감지

제곱근 블록과 같은 Math Function등의 특정 HISM 위반 검사

빠른 데드 로직 검사 활성화

전체 분석을 수행하기 위해 컴퓨팅 시간을 투자하기 전에 먼저 부분 데드 로직 검사를 실행하여 설계 시간에 가까운 오류를 디버깅

Bus Element지원

In Bus Element 또는 Out Bus Element 블록을 포함하는 맨 위 레벨 모델 분석

향상된 Dead Logic 리포팅

Results Inspector 창에서 단락 및 조건부 실행을 포함하여 데드 로직의 가능한 원인 보기

병렬 테스트 케이스 유효성 검사

병렬 컴퓨팅을 사용하여 테스트 사례 또는 반례 검증

이러한 기능 및 해당 함수에 대한 세부 정보는 릴리스 정보를 참조하십시오.

Simulink Design Verifier 추가 리소스