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

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Sep 01, 2006
Accession Number
ADA488111

Entities

People

  • Dan Casey
  • Mark Gerken
  • Ricky E. Sward

Organizations

  • United States Air Force Academy

Tags

Communities of Interest

  • Air Platforms
  • Autonomy
  • Cyber

DTIC Thesaurus Topics

  • Air Force
  • Aircrafts
  • Computer Network Security
  • Computer Programming
  • Computer Programs
  • Computer Science
  • Computers
  • Cybersecurity
  • Engineering
  • High Level Languages
  • Information Systems
  • Language
  • Programming Languages
  • Software Assurance
  • Software Development
  • Unmanned Aerial Vehicles
  • Vehicles

Fields of Study

  • Computer science
  • Engineering

Readers

  • Aerial Unmanned Vehicle Swarm Micro Periodontal Dentistry.
  • Computational Modeling and Simulation
  • Cybersecurity.

Technology Areas

  • Autonomy
  • Autonomy - Autonomous System Control