This supplement discusses the use of formal methods in the software life cycle for software that is produced in accordance with ED-12C. If the applicant is not planning to use formal analysis as defined in FM.1.6, then the applicant does not need to comply with this supplement.

PURPOSE

This supplement identifies the modifications and additions to ED-12C objectives, activities, explanatory text, and software life cycle data that should be addressed when formal methods are used as part of the software life cycle. This includes the artifacts that would be expressed using some formal notation and the verification evidence that could be derived from them.