The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.05 - Sept.-Oct. (2014 vol.16)
pp: 96-103
Seonmo Kim , Department of Computer Science and Engineering, University of Minnesota
Wonhong Nam , Department of Internet and Multimedia Engineering, Konkuk University
Hyunyoung Kil , Research Institute of Computer Information and Communication, Korea University
Myunghwan Park , Republic of Korea Air Force Academy
ABSTRACT
Military-related industries have developed many high-gravity aircraft, such as high-performance fighters and aerobatic aircrafts, which can maneuver beyond the acceleration tolerance limit of human beings. Gravity-induced loss of consciousness (GLOC) due to blood draining away from the brain is one of the main reasons for many high-gravity maneuvering aircraft accidents with many pilots losing their lives. Therefore, many automatic GLOC-monitoring systems have been proposed to prevent these accidents. However, it's not a trivial task to ensure system safety by ordinary simulation or testing methods. This article presents a case study to verify a GLOC monitoring system by using a model-checking technique. As a result of this verification, the authors report a case where the GLOC monitoring system misses, in which a pilot loses consciousness after some intentional movements.
INDEX TERMS
Formal verification, Computational modeling, Aircraft navigation, Military aircraft, Model checking, Mathematical model, Scientific computing,scientific computing, formal verification, aircraft, MATRIXx, symbolic model checking
CITATION
Seonmo Kim, Wonhong Nam, Hyunyoung Kil, Myunghwan Park, "Formal Verification of a Gravity-Induced Loss-of-Consciousness Monitoring System for Aircraft", Computing in Science & Engineering, vol.16, no. 5, pp. 96-103, Sept.-Oct. 2014, doi:10.1109/MCSE.2014.31
8 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool