Developing Safety Critical Software for an UnmannedAerial Vehicle Situational Awareness Tool

摘要

In this paper, we describe our application of the SPARKrnprogramming language to the development of flight controlrnsoftware for an Unmanned Aerial Vehicle (UAV). The SPARKrnlanguage was used during a senior-level software engineeringrncourse at the US Air Force Academy. This paper uses the yearlongrnproject from this course as an example application ofrnSPARK. The process we used to build an interface between C++rnand Ada is discussed along with our experiences with usingrnSPARK.