Accession Number:

ADA488111

Title:

When Computers Fly, It Has to Be Right: Using SPARK for Flight Control of Small Unmanned Aerial Vehicles

Descriptive Note:

Journal article

Corporate Author:

AIR FORCE ACADEMY COLORADO SPRINGS CO

Report Date:

2006-09-01

Pagination or Media Count:

6.0

Abstract:

One approach to software assurance is to use an annotated language such as SPARK. For safety critical software programs such as Unmanned Aerial Vehicle flight control software, the risk of software failure demands high assurance that the software will perform its intended function. Using an example from work being done at the U.S. Air Force Academy, this article describes SPARK and the formal process of proving correctness of software implementation.

Subject Categories:

  • Flight Control and Instrumentation
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE