Simulink Design Verifier

정형 기법을 사용한 오류 검출

시뮬레이션에서의 시맨틱 검사 또는 분석과 달리 Simulink Design Verifier에서 사용되는 정형 기법은 특정 동적 실행 시나리오의 발생 여부와 발생 조건을 알아낼 수 있습니다. 이러한 정보는 설계와 설계 요구사항을 개선하거나 시뮬레이션의 디버깅 및 검증을 안내하는 데 사용될 수 있습니다. Simulink Design Verifier는 다음과 같은 일반적인 설계 오류를 검출합니다. 정수 오버플로우, 0으로 나누기, 데드 로직(dead logic) 및 어설션(assertion) 위반.

정수 오버플로우 및 0으로 나누기 검출

Simulink Design Verifier의 설계 오류 검출 모드를 사용하여 정수 오버플로우 및 0으로 나누기를 검출할 수 있습니다. 분석은 자동화 되어 있으며 추가적인 사용자 입력이 필요 없습니다. 모든 블록에서 모든 신호에 대한 값의 허용 범위가 제공되어 문제의 근본 원인을 찾도록 도와줍니다. 분석이 끝나면 결과를 모델에서 직접 확인하거나 HTML 보고서에서 확인할 수 있습니다.

모델에서 블록은 녹색, 노란색 또는 빨간색으로 표시됩니다. 녹색 블록은 정수 오버플로우 또는 0으로 나누기등이 발생하지 않는다는 것이 증명되었다는 것입니다. 노란색 블록은 분석에서 확실한 결과를 얻을 수 없을 때 또는 분석의 시간 제한이 초과되었을 때 발생합니다. 모델 실행 경로에서 오류가 발견되면 정수 오버플로우나 0으로 나누기가 발생할 수 있는해당 경로의 모든 이후 블록은노란색으로 표시됩니다.

빨간색 블록은 설계 오류를 의미합니다. Simulink Design Verifier는 빨간색 블록에 대해 시뮬레이션 또는 테스트 시 문제를 재현할 수 있는 테스트 케이스를 생성합니다. Simulink에서 직접 테스트 케이스를 호출하고 시뮬레이션을 실행할 수 있습니다.

데드 로직(Dead Logic) 감지

Simulink Design Verifier의 테스트 생성 모드를 사용하여, 더 이상 사용되지 않거나 실행 중 활성화되지 않는 것으로 검증된 모델 객체를 의미하는 데드 로직(dead logic)을 검출할 수 있습니다. 데드 로직(dead logic)은 설계 오류 또는 요구사항 오류로 인해 발생하는 경우가 많습니다. 코드 생성 중에 데드 로직은 데드 코드로 이어집니다. 데드 로직은 시뮬레이션에서 수행하는 테스트만으로는 검출하기 어렵습니다. 다수의 시뮬레이션을 실행한 후에도 특정 동작이 활성화되지 않음을 증명하기는 어렵기 때문입니다.

테스트 생성 분석이 끝나면 테스트 생성 기준에 따라 모델의 색상이 지정됩니다. 시뮬레이션 중에 활성화될 수 없는 로직을 포함한 모델 객체는 빨간색으로, 시뮬레이션 중에 완전히 활성화될 수 있는 로직을 포함한 모델 객체는 녹색으로 표시됩니다. Simulink Design Verifier는 시뮬레이션 중에 데드 로직을 재현할 수 있는 테스트 케이스를 생성합니다.

Dead logic in a Stateflow chart detected by Simulink Design Verifier.
Simulink Design Verifier에 의해 빨간색으로 표시된 Stateflow 차트의 transition “press < zero_thresh” 조건이 절대로 false가 될 수 없기 때문에 이 transition에서 데드 로직이 발생합니다.

어설션(Assertion) 위반 검출

Simulink Design Verifier에서 속성 증명(property proving) 모드의 위반 검출 설정을 사용하여 어설션 위반을 검출합니다. Simulink Design Verifier는 분석 설정에서 지정된 시간 단계 수 내의 시뮬레이션 중에 어설션을 트리거할 수 있는 유효한 시나리오가 있는지 확인합니다. 예를 들어 역추진 작동기가 작동하고 비행 상태 표시기 값이 “true”가 될 때마다 트리거되는 어설션을 구성할 수 있습니다. 유효한 시나리오를 통해 위반될 수 있는 어설션은 빨간색으로 표시되며 이 어설션을 트리거하는 테스트 벡터가 생성됩니다. Simulink Design Verifier는 Simulink에서 이용 가능한 어설션 외에도 분석을 위한 제약을 정의하는 추가 블록을 제공하여 설계 동작을 철저하게 분석하고 시뮬레이션 실행 전에 설계 오류를 찾을 수 있게 합니다.

다음: 요구사항에 대한 설계 검증

평가판 사용 Simulink Design Verifier

평가판 신청

Track Design Changes with Requirements Traceability in MATLAB

온라인 세미나 보기