Date of Award

3-2023

Document Type

Thesis

Degree Name

Master of Science

Department

Department of Electrical and Computer Engineering

First Advisor

Kenneth M. Hopkinson, PhD

Abstract

Despite evidence that formal verification helps produce highly reliable and secure code, formal methods, i.e., mathematically based tools and approaches for software and hardware verification, are not commonly used in software and hardware development. The limited emphasis on formal verification in software education and training suggests that many developers have never considered the benefits of formal verification. Despite the challenging nature of their mathematical roots, software verification tools have improved; making it easier than ever to verify software. SPARK, a programming language and a formal verification toolset, is of particular interest for the AFRL, and will be a primary focus of this thesis. This thesis provides an overview of two safe and reliable languages with verification tools, namely SPARK and Rust. Then, to demonstrate the benefits of modern software verification tools, two examples of software verification in SPARK are presented. These examples include a verified implementation of the quaternion data structure and two implementations of Prim’s algorithm, to further demonstrate the usability and methodology of the SPARK verification toolset.

AFIT Designator

AFIT-ENG-MS-23-M-070

Comments

Approved for public release. Case number on file.

A 12-month embargo was observed.

Download

Share

COinS