Verification of flight software with karnough map-based checking

Link Jaw, W. T. Tsai, David Homan, Kirby Keller

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Citation (Scopus)

Abstract

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

Original languageEnglish (US)
Title of host publicationIEEE Aerospace Conference Proceedings
DOIs
StatePublished - 2007
Event2007 IEEE Aerospace Conference - Big Sky, MT, United States
Duration: Mar 3 2007Mar 10 2007

Other

Other2007 IEEE Aerospace Conference
CountryUnited States
CityBig Sky, MT
Period3/3/073/10/07

Fingerprint

Unmanned vehicles
Adaptive control systems
Flight control systems
Accreditation
Formal methods
Research laboratories
Air
Actuators
Decision making
Aircraft
Semiconductor materials
Control systems
Planning
Testing

ASJC Scopus subject areas

  • Aerospace Engineering

Cite this

Jaw, L., Tsai, W. T., Homan, D., & Keller, K. (2007). Verification of flight software with karnough map-based checking. In IEEE Aerospace Conference Proceedings [4161595] https://doi.org/10.1109/AERO.2007.352765

Verification of flight software with karnough map-based checking. / Jaw, Link; Tsai, W. T.; Homan, David; Keller, Kirby.

IEEE Aerospace Conference Proceedings. 2007. 4161595.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Jaw, L, Tsai, WT, Homan, D & Keller, K 2007, Verification of flight software with karnough map-based checking. in IEEE Aerospace Conference Proceedings., 4161595, 2007 IEEE Aerospace Conference, Big Sky, MT, United States, 3/3/07. https://doi.org/10.1109/AERO.2007.352765
Jaw L, Tsai WT, Homan D, Keller K. Verification of flight software with karnough map-based checking. In IEEE Aerospace Conference Proceedings. 2007. 4161595 https://doi.org/10.1109/AERO.2007.352765
Jaw, Link ; Tsai, W. T. ; Homan, David ; Keller, Kirby. / Verification of flight software with karnough map-based checking. IEEE Aerospace Conference Proceedings. 2007.
@inproceedings{a8992d175fdf498dad80da93a7eaedc5,
title = "Verification of flight software with karnough map-based checking",
abstract = "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",
author = "Link Jaw and Tsai, {W. T.} and David Homan and Kirby Keller",
year = "2007",
doi = "10.1109/AERO.2007.352765",
language = "English (US)",
isbn = "1424405254",
booktitle = "IEEE Aerospace Conference Proceedings",

}

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

BT - IEEE Aerospace Conference Proceedings

ER -