Ryan M. Baity

Date of Award

3-2021

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

First Advisor

Kenneth M. Hopkinson, PhD

Abstract

Software is an increasingly integral and sophisticated part of safety- and mission-critical systems. Poorly written software can lead to information leakage, undetected cyber breaches, and even human injury in cases where the software directly interfaces with components of a physical system. These systems may range from power facilities to remotely piloted aircraft. Software bugs and vulnerabilities can lead to severe economic hardships and loss of life in these domains. As fast as software spreads to automate many facets of our lives, it also grows in complexity. The complexity of software systems combined with the nature of the critical domains dependent on those systems results in a need to verify and validate the security and functional correctness of such software to a high level of assurance. The current generation of formal verification tools make it possible to write code with formal, machine-checked proofs of correctness. This thesis demonstrates the process of proving the correctness of code via a formal methods toolchain. It serves as a proof of concept for this powerful method of safety- and mission-critical software development.

AFIT Designator

AFIT-ENG-MS-21-M-009

DTIC Accession Number

AD1132199

Download

Share

COinS