DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click
HERE to register or log in.
Accession Number:
AD1132199
Title:
Formal Verification for High Assurance Software: A Case Study Using the SPARK Auto-Active Verification Toolset
Report Date:
2021-03-25
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.
Document Type:
Conference:
Journal:
Pages:
124
File Size:
2.69MB
Contracts:
Grants:
Distribution Statement:
Approved For Public Release
