ANSYS SCADE Suite Design Verifier and Formal Verification

Overview

This advanced training course presents formal verification techniques applied to ANSYS SCADE Suite models using ANSYS SCADE Suite Design Verifier.

ANSYS SCADE Suite Design Verifier is a formal verification tool to formally express and assess safety requirements, and effectively find bugs early in the development process. ANSYS SCADE Suite Design Verifier automatically produces a counter-example when a proof objective is not satisfied by the ANSYS SCADE Suite model under analysis. This tool can also be used to find divisions by zero operations as well as underflow/overflow errors in ANSYS SCADE Suite models.

The course also offers a specific focus on writing verification properties with ANSYS SCADE Suite Design Verifier.

Prerequisites

• Basic knowledge of formal verification methods and ANSYS SCADE Suite.

Target Audience: Software Engineers / Verification Engineers

Teaching Method: Lectures and computer practical sessions to validate acquired knowledge. A training certificate is provided to all attendees who complete the course.

Core Topics

• Formal verification in application development process with ANSYS SCADE Suite
• Getting started with ANSYS SCADE Suite Design Verifier
• Writing properties
• Verification with data
• Methodology