This full-day training course provides an introduction to methods and software tools that can be used to produce verification results suitable for use in certification. Collectively known as “formal methods,” these methods and tools are based on elements of discrete mathematics such as symbolic logic and set theory.
A variety of different kinds of formal methods will be described in this training, including model-checking, theorem-proving, satisfiability solving, program verification and abstract interpretation. Software tools that support such methods will be demonstrated along with detailed examples. Participants will learn how to choose an appropriate kind of formal method for specific objectives, along with strategies for integrating the use of formal methods into the overall software development process.
Prior knowledge of formal methods is not necessary to benefit from this training course. However, it will be assumed that participants are familiar with the fundamental elements of a software development process such as the specification of system and software requirements, and requirements-based testing.
While designed for the airborne software industry, this training should also be of interest to individuals from other industries such as automotive and rail signaling where formal methods can also be used to specify, analyze and verify software functionality.