Simulink Design Verifier


주요 특징

  • 조건(condition), 결정(decision) 및 MCDC 등 기능 요구사항 및 모델 커버리지 목표로부터 테스트 케이스 입력 생성
  • 데드 로직(dead logic), 정수 및 고정 소수점 오버플로우, 0으로 나누기(division by zero) 및 설계 요구 사항 위반(violations of design requirement) 감지
  • 기능 및 안전 요구 사항을 모델링하기 위한 검증 블록
  • 분석 및 디버깅을 위한 위반 사례를 생성하여 속성 증명
  • 대규모 모델에서 기능 종속성 및 문제가 있는 동작을 분석하기 위한 Model Slicer
  • 고정 및 부동 소수점 모델을 위한 Polyspace® 및 Prover® 정형 검증 엔진
Identify design errors, generate test cases, and verify designs against requirements using Simulink Design Verifier™.

Simulink Design Verifier™를 사용하면 코드를 생성하지 않고도 초기에 설계를 확인하고 요구 사항을 검증할 수 있습니다. 이를 통해 Simulink® 환경에서의 설계 견고성(robustness)이 향상됩니다. 수학적으로 엄격한 정형 기법을 사용하여 제어 로직, S-function 및 MATLAB® 코드를 분석할 수 있습니다. 테스트 시나리오 및 예상되는 결과가 구체적인 데이터 값으로 표현되는 기존의 테스팅 방식과 달리, 정형 검증 기법을 사용하면 그 대신 시스템 거동에 대한 모델을 통해 작업이 가능합니다. 정형 검증은 소프트웨어에 런타임 오류가 있는지의 여부 등과 같은 특정 소프트웨어 속성을 증명하여 시스템 요구 사항을 세밀하게 파악할 수 있습니다.


설계 오류 검출

Simulink Design Verifier를 통해 특정 동적 실행 시나리오가 발생하는지의 여부 및 어떤 상황에서 발생하는지를 확인할 수 있습니다. 이를 통해 정수 오버플로, 0으로 나누기(division by zero), 데드 로직(dead logic) 및 범위를 벗어난 배열 등의 설계 오류를 검출할 수 있습니다. 설계 주기에서 시뮬레이션 기반 테스팅을 수행하기 전 초기 단계에 이러한 오류를 발견하면 추후의 수정 비용을 방지할 수 있습니다.

설계 오류 검출은 완전히 자동으로 이루어지므로 모델에서 직접 또는 HTML 보고서를 통해 결과를 확인할 수 있습니다. 모든 블록 내 모든 신호의 허용 범위를 통해 문제가 유발된 근본 원인을 찾을 수 있습니다. 모델에서 블록은 녹색, 오렌지색 또는 빨간색으로 표시되고 녹색은 검출된 오류 없음, 오렌지색은 제공된 시간 내에 분석 결과가 불충분 함을, 빨간색은 블록에 설계 오류가 있음을 나타냅니다. Simulink Design Verifier는 테스트 케이스 입력을 자동으로 생성하여 각 빨간색 블록에 대한 오류 시나리오를 재생성합니다. Simulink에서 이러한 테스트 입력을 사용하면 오류가 발생하는 상황을 파악하여 디버그를 수행할 수 있습니다.

설계 오류 검출. 설계 오류가 있는 블록은 빨간색으로 강조 표시되고 올바른 서브시스템은 녹색으로 강조 표시됩니다.

데드 로직(Dead Logic) 검출

데드 로직 검출 모드는 사용되지 않거나 실행 도중 비활성 상태를 유지하는 모델의 객체를 탐색합니다. 데드 로직은 종종 설계 또는 요구 사항 오류로 인해 발생할 수 있습니다. 코드 생성 도중 데드 로직으로 인해 데드 코드가 발생할 수 있습니다. 시뮬레이션에서 활성화될 수 없는 로직을 포함하고 있는 모델 객체는 빨간색으로 표시되고 시뮬레이션에서 완전 활성화될 수 있는 로직을 포함하고 있는 모델 객체는 녹색으로 표시됩니다. 매우 여러 차례 시뮬레이션을 수행한 이후에도 특정 동작이 활성화될 수 없는지를 결정하는 것은 어렵기 때문에 시뮬레이션을 통한 테스트만으로 데드 로직을 검출하는 것은 어렵습니다.

Simulink Design Verifier로 검출된 Stateflow 차트의 transition에 대한 데드 로직은 빨간색으로 강조 표시됩니다. “press < zero_thresh” 조건은 false가 될 수 없기 때문에 이러한 transition에서 데드 로직이 발생할 수 있습니다.

테스트 케이스 입력 생성

구현 모델의 입출력 동작만을 검증한다고 해서 설계의 정확성이 보장되는 것은 아닙니다. 모델 검증을 위해서는 기능 테스트가 처음 단계에서 수행되어야 하지만 본질적으로 이러한 테스트는 불완전할 가능성이 있는 요구 사항으로부터 얻어집니다. 설계의 견고성을 높이기 위해서는 모델 커버리지 등과 같은 구조적인 검증 기법을 사용하여 모델에서 사용되지 않는 시뮬레이션 경로를 발견해야 합니다. 본질적으로 모델 커버리지는 테스트 케이스가 모델을 완전하게 실행하는 방법을 측정하고 테스트 케이스가 실행하는 경로의 비율을 보여줍니다. 테스트되지 않은 경로를 조사함으로써 잠재적인 설계 오류를 발견할 수 있습니다.

Simulink Design Verifier™에서 테스트 생성 용도로 정형 기법을 사용한 기존 테스트 케이스 활용 및 전체 커버리지 달성

Simulink Design Verifier에서는 정형 기법과 경험적 기법을 조합하여 모델 커버리지 및 사용자 기정 기준을 생성합니다. 모델 커버리지를 위한 테스트 케이스 생성은 직접 작성되었거나 전체 시스템의 시뮬레이션 동안 수집된 요구 사항 기반 테스트 입력을 확장합니다. 조건(condition), 결정(decision) 및 MCDC 커버리지용 커버리지 객체뿐만 아니라 사용자 지정 테스트 객체를 지정하여 요구 사항 기반 테스트 케이스를 생성할 수 있습니다.

Simulink Design Verifier™를 사용하여 시스템 요구 사항 모델로부터 테스트 케이스를 생성합니다.

Test Generation Advisor를 사용하여 테스트를 생성하기 위한 모델 컴포넌트(atomic 서브시스템 및 모델 블록)를 선택할 수 있습니다. Generation Advisor는 고수준 분석을 수행하여 테스트를 생성하기 이전에 특히 대규모 모델, 복잡 모델 또는 테스트 생성 호환성이 불확실한 모델 등에 대해 깊이 이해할 수 있도록 도와줍니다. 생성된 모든 테스트 케이스 입력은 시뮬레이션, SIL 또는 PIL에서 테스트 실행을 위한 입력으로 직접 사용될 수 있는 MATLAB 구조체 형태로 수집됩니다. 또한, 수집된 테스트 케이스는 Simulink Test™와 함께 사용되고 테스트 하네스와 연관될 수 있습니다. 테스트 수행 도중 코드 커버리지를 수집하기 위한 용도로 Embedded Coder®에서 사용할 수 있는 타사 코드 커버리지 툴을 통합하는 것도 가능합니다.

Simulink Design Verifier는 ISO 26262, IEC 61508 또는 EN 50128 표준을 준수해야 하는 프로세스를 개발하는 용도로 TÜV SÜD로부터 인증을 취득했습니다.

Test Generation Advisor: 테스트 생성 호환성, 커버리지 목표 및 모델의 데드 로직과 모델 컴포넌트 계층 구조 보기 요약

Model Slicer를 통한 문제가 있는 동작 격리

Simulink Design Verifier는 동적 및 정적 분석을 조합하여 종속성을 추적함으로써 모델 내에서 관심이 있는 동작을 격리합니다. 종속성 분석에는 블록, 신호 및 모델 컴포넌트 종속성 결정이 포함됩니다. 계층 구조 수준 및 설계 복잡성이 있는 대규모 모델의 경우 이는 시간이 오래 걸리는 프로세스입니다. Model Slicer를 사용하면 모델의 어느 부분이 특정 동작에 영향을 주는지를 파악할 수 있습니다. 정적 분석을 사용하면 모든 가능한 시뮬레이션 경로에 대한 모델 종속성을 식별할 수 있는 반면 시뮬레이션 기반 분석을 사용하면 시뮬레이션 도중 활성 경로만이 강조 표시됩니다.

종속성 분석은 시작 지점에서 상향, 하향 또는 양방향으로 수행됩니다. 이를 통해 포트, 신호 및 블록의 기능 종속성을 강조 표시 및 추적하고 대규모 모델을 독립적인 소형 분석 모델로 나눌 수 있습니다. 또한, 다양한 스위치 및 로직 블록을 통해 서브시스템 출력 및 신호 경로에 영향을 주는 블록을 확인할 수 있습니다.

복잡한 모델 테스트 및 디버그 모델 내의 관심 영역을 식별하고 추후 분석 및 디버깅을 위해 조각화된 모델을 생성합니다.

요구사항 기반 검증

특정 기능 또는 안전 요구 사항에 따라 동작하는 설계를 정형적으로 검증하기 위해서는 우선 요구 사항 명령이 사람이 사용하는 언어에서 정형 분석 엔진이 이해할 수 있는 언어로 변환되어야 합니다. Simulink Design Verifier는 MATLAB 함수, Simulink 및 Stateflow®을 사용하여 정형 요구 사항을 표현할 수 있는 기능을 제공합니다. Simulink내의 각 요구 사항은 연관된 검증 목표를 하나 이상 가짐니다. 요구 사항 및 검증 목표가 파악되면 정형 기법을 통해 설계 정확성을 증명하기 위한 용도로 사용될 수 있습니다.

예를 들어, 비행 추적 시스템에서는 역추진 액추에이터가 사용되고 비행 상태 표시기의 값이 "true"일 때마다 트리거되는 어셜션(assertion) 또는 증명 목표가 구성될 수 있습니다. Simulink Design Verifier는 원치 않은 동작을 유발할 수 있는 모든 가능성이 있는 입력 조건을 검사한 후 발견 사항을 보고합니다. 제공된 증명 목표와 관련하여 설계는 유효한 것으로 증명되거나 안전 요구 사항을 위반하는 것으로 검출될 수 있습니다. 위반 사항이 검출되면 Simulink Design Verifier는 시뮬레이션에서 위반 사항을 시연할 수 있는 테스트 케이스를 생성합니다.

Simulink Verification and Validation™에서 Requirements Management Interface와 함께 Simulink Design Verifier를 사용하는 경우 요구 사항 및 Simulink 이외의 고수준 텍스트 요구 사항에 대한 검증 목표를 수집하기 위해 사용된 블록 및 함수를 연결할 수 있습니다.

증명 목표에서 제시된 안전 요구 사항과 관련하여 설계를 검증하기 위한 Simulink Design Verifier 보고서 이 보고서는 설계가 올바르다고 증명되어야 하는 목표 목록 및 분석을 통해 발견되어야 하는 반례 목표(counterexample) 목록을 보여줍니다.