This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
1st Workshop on Industrial-Strength Formal Specification Techniques
Adding formal specifications to a proven V&V process for system-critical flight software
Boca Raton, Florida
April 05-April 08
ISBN: 0-8186-7005-3
ASCII Text
x 
 
J. Hagar, J.M. Bieman, "Adding formal specifications to a proven V&V process for system-critical flight software," Industrial-Strength Formal Specification Techniques, Workshop on, pp. 76, 1st Workshop on Industrial-Strength Formal Specification Techniques, 1995.
 
 
BibTex
x
 
@article{ 10.1109/WIFT.1995.515480,
author = {J. Hagar and J.M. Bieman},
title = {Adding formal specifications to a proven V&V process for system-critical flight software},
journal ={Industrial-Strength Formal Specification Techniques, Workshop on},
volume = {0},
year = {1995},
isbn = {0-8186-7005-3},
pages = {76},
doi = {http://doi.ieeecomputersociety.org/10.1109/WIFT.1995.515480},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Industrial-Strength Formal Specification Techniques, Workshop on
TI - Adding formal specifications to a proven V&V process for system-critical flight software
SN - 0-8186-7005-3
SP
EP
A1 - J. Hagar,
A1 - J.M. Bieman,
PY - 1995
KW - safety-critical software; aircraft computers; aircraft control; formal specification; program verification; program testing; system-critical flight software; formal specifications; flight avionics control systems; validation; verification; Anna formal specification language; supporting tool set; Test Range Oracle Tool; TROT; equation execution; testing process; test coverage
VL - 0
JA - Industrial-Strength Formal Specification Techniques, Workshop on
ER -
 
J. Hagar, Martin Marietta Astronaut. Co, Denver, CO, USA
J.M. Bieman, Martin Marietta Astronaut. Co, Denver, CO, USA
The process used to validate, verify, and test flight avionics control systems has produced software that is highly reliable. However, ever greater demands for reliability require new automated tools to improve existing processes. We used the Anna formal specification language and supporting tool set to develop a Test Range Oracle Tool (TROT) to automate the testing of equation execution. Our approach fits within the existing testing process and can increase the level of test coverage without increasing testing costs. The TROT approach introduces the use of formal specification languages and supporting tools to an existing industry program. This approach is being evaluated for expansion into other test support areas.
Index Terms:
safety-critical software; aircraft computers; aircraft control; formal specification; program verification; program testing; system-critical flight software; formal specifications; flight avionics control systems; validation; verification; Anna formal specification language; supporting tool set; Test Range Oracle Tool; TROT; equation execution; testing process; test coverage
Citation:
J. Hagar, J.M. Bieman, "Adding formal specifications to a proven V&V process for system-critical flight software," wift, pp.76, 1st Workshop on Industrial-Strength Formal Specification Techniques, 1995
Usage of this product signifies your acceptance of the Terms of Use.