ANSYS SCADE Suite Design Verifier and Formal Verification

Overview

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.

This advanced training course presents the static formal verification concept to perform verification of ANSYS SCADE Suite applications. You will learn to insert mathematical reasoning into the verification processes and to add completeness to classical testing by detecting uncovered bugs. 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.