Course 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 software requirements, and effectively find bugs early in the development process.
This tool can check the use of arithmetic operators: it verifies if divisions by zero, invalid operations (Not a Number = NaN) as well as overflow errors can occur in Ansys SCADE Suite models.
Ansys SCADE Suite Design Verifier uses the Prover-PSL © engine to analyze a property and automatically produces a counter-example (scenario file) when a proof objective is not satisfied by the Ansys SCADE Suite model under verification.
Core Topics
- Formal verification in application development process with Ansys SCADE Suite
- Perform predefined property verifications (such as divisions by zero, NaN values, overflow errors)
- Perform user property verifications (express and analyze user properties from software requirements)
Prerequisites
- Basic knowledge of formal verification methods and Ansys SCADE Suite.
Teaching Method
Lectures and computer practical sessions to validate acquired knowledge. A training certificate is provided to all attendees who complete the course.