Bibliographic Details
| Title: |
When Computers Fly, It Has to Be Right: Using SPARK for Flight Control of Small Unmanned Aerial Vehicles. |
| Authors: |
Sward, Ricky E.1 ricky.sward@wavmax.com, Gerken, Mark1 mark.gerken@usafa.af.mil, Casey, Dan1 daniel.casey@ramstein.af.mil |
| Source: |
CrossTalk: The Journal of Defense Software Engineering. Sep2006, Vol. 19 Issue 9, p10-14. 5p. 3 Diagrams. |
| Subjects: |
SPARK (Computer program language), Computer software, Computer systems, Computer industry, Software failures, System failures |
| Geographic Terms: |
United States |
| 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 implementations. [ABSTRACT FROM AUTHOR] |
|
Copyright of CrossTalk: The Journal of Defense Software Engineering is the property of USAF Software Technology Support Center and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
