Formal Methods

Certification Objectives

Theorem Proving

Model Checking

Abstract Interpretation

Formal Notation

Syntax & Semantics

Unambiguous

Mathematically Defined

Sound Analysis

Assumptions Justifications

High Level Requirements

Low Level Requirements

Software Architecture

Source Code Verification

FGS - Flight Guidance System Synchronization

Single FGS Channel Mode Logic

Specify Requirements in Formal Language

FGS Control Law

Non Functional Requirements Check

Case Study

General Description

Verification Approach Description

PVS - Prototype Verification System

Tools

Software Verification Plan

Overview

Case Study Functionality

Qualification Required

Life Cycle Data

Overview

Software Verification Plan

Formal Specification and Verification Tools

Life Cycle Data Items

Objectives to Be Satisfied

Formal Verification