Seonmo Kim , Konkuk University, Seoul
Wonhong Nam , Konkuk University, Seoul
Hyunyoung Kil , Korea University, Seoul
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/MCSE.2014.31
Military industry has developed many high-gravity maneuvering aircraft, such as high performance fighters and aerobatic aircrafts, which can maneuver beyond the acceleration tolerance limit of human being. Since this high-gravity maneuvering may cause pilots a loss of consciousness due to draining blood away from the brain, the Gravity-induced Loss of Consciousness (GLOC) is one of the main reasons for many high-gravity maneuvering aircraft accidents where many pilots have lost their lives. Therefore, many automatic GLOC monitoring systems have been proposed to prevent these accidents. However, it is not trivial to ensure the safety of the system by ordinary simulation or testing methods. In this paper, we present a novel approach to verify the GLOC monitoring system by using model checking technique. As a result of verification, we report a error case that the GLOC monitoring system misses, in which a pilot loses his consciousness after some intentional movements.
Seonmo Kim, Wonhong Nam, Hyunyoung Kil, "Formal Verification of Gravity-induced Loss of Consciousness Monitoring System for Aircraft", Computing in Science & Engineering, , no. 1, pp. 1, PrePrints PrePrints, doi:10.1109/MCSE.2014.31