Simulink Design Verifier

주요 특징

  • Polyspace® 및 Prover Plug-In® 형식 분석 엔진
  • 데드 로직(dead logic), 정수 및 고정 소수점 오버플로우, 0으로 나누기 및 설계 속성 위반 검출
  • 기능 및 안전 요구사항을 모델링하기 위한 블록 및 함수
  • 기능 요구사항 및 condition, decision 및 modified condition/decision(MCDC)을 포함한모델 커버리지 목표로부터 테스트 벡터 생성
  • 분석 및 디버깅을 위한 위반 사례를 생성하여 속성 증명(Property Proving)
  • 고정 소수점 및 부동 소수점 모델 지원

Simulink Design Verifier를 통해 Simulink® 환경 내에서 모델 분석을 수행할 수 있습니다. 코드를 생성할 필요 없이 초기 단계에서 설계 및 요구사항을 검증할 수 있습니다. 따라서 설계 프로세스 전반에서 확인 및 검증을 수행할 수 있습니다. Simulink Design Verifier를 통한 모델 분석은 시뮬레이션 결과를 정형 기법을 통한 분석에 대한 입력으로 사용할 수 있게 함으로써 시뮬레이션을 보완합니다.

Simulink Design Verifier는 임베디드 제어 설계에서 일반적으로 사용되는 Simulink 및 Stateflow®의 이산 시간 서브세트를 지원합니다.

Design error detection in a model using Simulink Design Verifier.
Simulink Design Verifier를 사용한 모델의 설계 오류 검출 설계 오류가 있는 블록은 빨간색으로, 올바른 것으로 증명된 서브시스템은 녹색으로 표시되어 있습니다.

모델 기반 설계의 정형 기법

Simulink Design Verifier는 Prover Technology의 Prover Plug-In과 Mathworks의 Polyspace 정형 분석 엔진이 제공하는 정형 분석 기술을 사용합니다. 이러한 기술은 수학적으로 엄격한 절차를 사용하여 테스트 케이스 및 반례에 대해 모델의 가능한 실행 경로를 검색합니다. 테스트 시나리오와 예상 결과가 구체적인 데이터 값으로 표현되는 기존의 테스트 방식과 달리 정형 분석 기술에서는 구체적인 데이터 값이 아닌 시스템 동작 모델을 사용하여 작업할 수 있습니다. 시스템 동작 모델은 원하는 시스템 동작과 원하지 않는 시스템 동작을 설명하는 테스트 시나리오 및 검증 목표에 대한 모델을 포함할 수 있습니다. 이러한 모델을 통해 형식 분석을 수행하면 시뮬레이션을 보완하고 설계를 더욱 잘 이해할 수 있습니다.

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

시뮬레이션에서의 시맨틱 검사 또는 분석과 달리 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에서 기능 요구사항 표현

설계가 이러한 요구사항에 따라 동작함을 공식적으로 확인하려면 요구사항 진술을 먼저 사람의 언어에서 정형 분석 엔진이 이해하는 언어로 변환해야 합니다. Simulink Design Verifier는 Simulink, MATLAB® 함수 및 Stateflow를 사용하여 정형 요구사항을 표현할 수 있게 합니다. Simulink의 각 요구사항에는 하나 이상의 검증 목표가 연결되어 있습니다. 이러한 검증 목표는 설계가 기능 및 안전 요구사항을 충족하는지 리포트하기 위해 사용됩니다.

Simulink Design Verifier는 검증 목표를 정의하고 구성하는 데 사용할 수 있는 빌딩 블록 및 함수 세트를 제공합니다. 제공된 블록 라이브러리에는 테스트 목표, 증명 목표, 어설션, 제약에 대한 블록 및 함수와 함께 시간적 측면의 검증 목표의 모델링을 위한 전용 시간 연산자(temporal operator) 세트가 포함됩니다.

개별 요구사항과 관련된 검증 목표를 라이브러리로 그룹화하여 설계와 별도로 관리하고 검토할 수 있습니다.

Simulink Design Verifier library of property examples.
Simulink Design Verifier 속성 예제 라이브러리.

Simulink Design Verifier를 Simulink Verification and Validation™의 Requirements Management Interface와 함께 사용하는 경우 요구사항 및 검증 목표 캡처에 사용되는 블록과 함수를 Simulink 외부의 고수준 텍스트 요구사항에 링크를 만들 수 있습니다.

요구사항에 대한 설계 검증

일단 검증 모델에서 캡처된 요구사항 및 검증 목표는 정형 기법을 사용하여 설계의 정확성을 증명하는 데 사용할 수 있습니다.

기능 요구사항을 검증하고 시스템을 원하는 상태로 유도하기 위해 Test Objective 블록과 MATLAB 함수를 사용하여 테스트 목표를 정의할 수 있습니다. 테스트 생성 중에 Simulink Design Verifier는 지정된 목표를 충족하는 유효한 테스트 케이스를 찾으려고 시도합니다. 목표를 충족할 수 없는 경우 설계는 주어진 분석 제약 조건들에 대해 필요한 기능을 수행할 수 없다는 것을 의미합니다.

안전 요구사항에 대한 설계의 정확성을 검증하려면 Proof Objective 블록과 MATLAB 함수를 사용하여 증명 목표를 정의할 수 있습니다. 분석 과정에서 Simulink Design Verifier는 원치 않는 동작을 일으킬 수 있는 모든 가능한 입력 조건을 검사한 후 결과를 리포트합니다. 주어진 증명 목표에 대해 설계는 유효한 것으로 검증될 수도 있고 안전 요구사항을 위반하는 것으로 드러날 수도 있습니다. 위반이 감지되면 Simulink Design Verifier는 시뮬레이션에서 위반을 보여줄 수 있는 테스트 벡터를 생성합니다.

Simulink Design Verifier report for verifying a design against safety requirements represented with proof objectives.
Simulink Design Verifier는 증명 목표로 표현된 안전 요구사항에 대한 설계 검증을 리포트합니다. 이 리포트는 설계가 유효한 것으로 증명된 목표 목록과 반례가 발견된 목표 목록을 표시합니다.

분석 결과 검증

Simulink, MATLAB 함수 및 Stateflow로 표현된 요구사항을 설계와 병행하여 시뮬레이션할 수 있습니다. 또한 이를 통해 생성된 코드를 검증하여 SIL 모드 또는 PIL 모드에서 통합 시뮬레이션을 수행할 수도 있습니다. 모델 커버리지 툴은 시뮬레이션 동안 검증 목표의 활성화에 관한 정보를 축적하고 커버리지 결과를 Simulink Design Verifier 커버리지 메트릭을 통해 제공합니다. 안전 요구사항을 표현하는 proof objectives를 사용하여 위반 발생 즉시 시뮬레이션을 중단함으로써 근본 원인 분석 및 디버깅을 가속할 수 있습니다.

모델 커버리지 분석

Simulink Design Verifier는 SimulinkStateflow 모델의 알고리즘과 로직을 분석하여 고무결성(high-integrity) 시스템 개발을 위한 산업 표준에 요구되는 테스트 케이스와 매개변수를 생성할 수 있습니다. 구조적 커버리지 기준을 위한 테스트 생성에는condition, decision 및 modified condition/decision(MC/DC)이 포함됩니다.

테스트 생성

모델 커버리지를 위한 테스트 생성은 수동으로 작성되었거나 전체 시스템의 시뮬레이션 중에 수집된 요구사항 기반 테스트를 보강합니다. Simulink Design Verifier는 이 접근 방식을 통해 기존 모델 커버리지 정보를 가져오고 요구사항 기반 테스트 중에 충족되지 못한 모든 커버리지 목표를 충족하는 추가 테스트 벡터를 생성할 수 있습니다.

Visual display of a generated test vector that activates previously untested functionality.

이전에 테스트되지 않은 기능을 활성화시키는 생성된 테스트 벡터를 시각적으로 표시

이러한 테스트 벡터를 사용하여 누락된 요구사항을 좀 더 잘 이해하고 더욱 완전한 테스트 하네스를 만들 수 있습니다. Simulink Design Verifier는 다수의 인포트 및 아웃포트를 갖는 모델의 테스트를 단순화하기 위해 미사용 신호를 파악하고 자동으로 테스트 하네스에서 제거합니다.

모든 생성된 테스트 벡터는 MATLAB 구조체 변수로 캡처되어 시뮬레이션, SIL 또는 PIL에서 테스트 실행을 위한 입력으로 직접 사용할 수 있습니다. 수집된 테스트 데이터는 테스트 하네스 모델을 생성하는 데도 사용할 수 있습니다.

생성된 테스트 벡터의 검증

구조적 커버리지 기준을 충족하는 생성된 테스트 벡터를 검증하기 위해 Simulink Verification and Validation에서 제공되는 모델 커버리지 툴을 사용할 수 있습니다. 이 툴은 시뮬레이션을 모니터링하고 정형 분석 중에 리포트된 목표가 달성되었는지 측정합니다. Model Coverage Tool은condition, decision 및 MC/DC 커버리지에 대한 커버리지 목표뿐 아니라 테스트 목표, 증명 목표, 가정, 제약, Lookup Table 및 시뮬레이션 중 기록된 신호 범위에 대한 커버리지도 보고합니다.

Simulink Design Verifier는 ISO 26262, IEC 61508 또는 EN 50128 표준을 반드시 준수해야 하는 개발 프로세스에서 사용할 수 있도록 TÜV SÜD의 인증을 받았습니다.

생성된 코드에 대한 테스트 커버리지 분석

Simulink Design Verifier는 SIL 및 PIL의 코드에 대해 생성된 테스트 케이스의 실행을 자동화하는 테스트 자동화 기능을 제공합니다. Simulink Design Verifier의 코드 검증 기능을 사용하려면 Embedded Coder™가 필요합니다. 테스트 실행 중에 Embedded Coder에서 이용 가능한 코드 커버리지 툴을 통합하여 코드 커버리지를 수집할 수 있습니다.

Designing Supervisory Control for Safety-Critical Systems

웨비나 보기