DocumentCode :
3493550
Title :
Proving correctness of unmanned aerial vehicle cooperative software
Author :
Sward, Ricky E.
Author_Institution :
Dept. of Comput. Sci., US Air Force Acad., Colorado Springs, CO, USA
fYear :
2005
fDate :
19-22 March 2005
Firstpage :
767
Lastpage :
771
Abstract :
As unmanned aerial vehicles (UAVs) become more prevalent, it is important to show that the software being used to control the UAVs has been built correctly. An error in the UAV auto-pilot or navigation system could result in the destruction of the UAV or objects on the ground. The purpose of this research is to develop a software application that will control the cooperation between two UAVs during reconnaissance. This application is being developed using formal methods in software engineering to prove the correctness of the software. The SPARK programming language provides techniques for building correct software applications and proofs of their correctness without relying on extensive testing. The SPARK language is a powerful application of formal methods to the area of safety-critical systems.
Keywords :
aerospace computing; aircraft; aircraft navigation; programming languages; remotely operated vehicles; safety-critical software; software engineering; SPARK programming language; UAV autopilot system; formal methods; navigation system; safety-critical systems; software engineering; unmanned aerial vehicle cooperative software; Application software; Computer languages; Navigation; Real time systems; Reconnaissance; Software engineering; Software safety; Software testing; Sparks; Unmanned aerial vehicles;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Networking, Sensing and Control, 2005. Proceedings. 2005 IEEE
Print_ISBN :
0-7803-8812-7
Type :
conf
DOI :
10.1109/ICNSC.2005.1461287
Filename :
1461287
Link To Document :
بازگشت