TY - GEN
T1 - Verification of flight software with karnough map-based checking
AU - Jaw, Link
AU - Tsai, W. T.
AU - Homan, David
AU - Keller, Kirby
PY - 2007
Y1 - 2007
N2 - Future U.S. Air Force capabilities will rely on mixed manned/unmanned vehicles working together as a team. These vehicles will be increasingly autonomous, capable of on-board decision-making and mission re-planning, and yet interoperable to complete a desired mission safely, reliably, and adaptively. A key enabler of this cooperative airspace is adaptive or reconfigurable control software. This kind of software poses a strong challenge to the verification and validation (V&V) process, which leads to the final certification and accreditation of the software. Traditional V&V processes rely heavily on testing or other informal methods. These processes are time consuming and increasingly expensive as the complexity of the software increases. Alternative processes that can increase affordability while applying more formal methods have been attractive recently. This paper describes a formal software checking method by using the Karnaugh Map technique. This method checks the consistency and completeness of the software during the verification process. A proof-of-concept test of the method has been applied to an aircraft actuation system. The C-language source code of the actuator system used as a model in an adaptive flight control system is checked by the method. The preliminary results of this proof of concept are presented in this paper. The results demonstrated the feasibility of the method. The results are consistent with previous applications of the method to other sophisticated software systems, such as semiconductor manufacturing and command & control systems. Continued maturation of this process and technology is being supported by the Air Force Research Laboratory
AB - Future U.S. Air Force capabilities will rely on mixed manned/unmanned vehicles working together as a team. These vehicles will be increasingly autonomous, capable of on-board decision-making and mission re-planning, and yet interoperable to complete a desired mission safely, reliably, and adaptively. A key enabler of this cooperative airspace is adaptive or reconfigurable control software. This kind of software poses a strong challenge to the verification and validation (V&V) process, which leads to the final certification and accreditation of the software. Traditional V&V processes rely heavily on testing or other informal methods. These processes are time consuming and increasingly expensive as the complexity of the software increases. Alternative processes that can increase affordability while applying more formal methods have been attractive recently. This paper describes a formal software checking method by using the Karnaugh Map technique. This method checks the consistency and completeness of the software during the verification process. A proof-of-concept test of the method has been applied to an aircraft actuation system. The C-language source code of the actuator system used as a model in an adaptive flight control system is checked by the method. The preliminary results of this proof of concept are presented in this paper. The results demonstrated the feasibility of the method. The results are consistent with previous applications of the method to other sophisticated software systems, such as semiconductor manufacturing and command & control systems. Continued maturation of this process and technology is being supported by the Air Force Research Laboratory
UR - http://www.scopus.com/inward/record.url?scp=34548754995&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=34548754995&partnerID=8YFLogxK
U2 - 10.1109/AERO.2007.352765
DO - 10.1109/AERO.2007.352765
M3 - Conference contribution
AN - SCOPUS:34548754995
SN - 1424405254
SN - 9781424405251
T3 - IEEE Aerospace Conference Proceedings
BT - 2007 IEEE Aerospace Conference Digest
T2 - 2007 IEEE Aerospace Conference
Y2 - 3 March 2007 through 10 March 2007
ER -