Formal Verification of a Merge Sort Algorithm in SPARK
Ryan Baity, Laura R. Humphrey, Kenneth Mark Hopkinson · AIAA Scitech 2021 Forum · 2021
View Video Presentation: https://doi.org/10.2514/6.2021-0039.vid Sophisticated software is enabling new capabilities across a number of different domains, from driverless cars in the automotive industry, to embedded medical devices in the healthcare industry, to autonomous drones in the aerospace industry. Given the safety implications, there is a need for software in these domains to be highly reliable. However, there are concerns that verification through testing alone will be insufficient to demonstrate the required degree of software reliability, since testing will only be able to cover a small portion of all possible software behaviors. An alternative is to analyze software through formal methods, i.e. mathematically-based tools and techniques for design and verification. Formal methods can be used to check many types of properties, including functional correctness of software, i.e. that software complies with a user-generated specification describing its intended behavior. The goal of this paper is to give the reader an impression of what is involved in proving functional correctness of a software module by walking through a simple example in an appropriate tool. To that end, we go through the process of proving functional correctness of a simple well-known merge sort algorithm in SPARK, a programming language with an associated verification toolset that has been used to create highly assured software in a number of domains, including the aerospace domain.