Systems that make safety-critical decisions must undergo a rigorous verification and validation process to ensure automation decisions do not jeopardize the nominal safe state of operation. Flight safety assessment and management is a high-level decision-making system to reduce loss of control risk. This paper demonstrates how tools from formal verification can be used to guide the design of a takeoff flight safety assessment and management system implemented as a deterministic Moore machine. Finite state abstractions of simplified takeoff dynamics under different control authorities (i.e., pilot vs safety controller) are computed and composed with the Moore machine. By construction, the composition captures all behaviors of simplified takeoff dynamics. Then, a model checking tool analyzes whether this composition satisfies the takeoff safety requirements specified by federal aviation regulations. The results of model checking together with the abstraction are used to refine the Moore machine to ensure satisfaction of the specification. This paper contributes a novel approach to verification of a supervisory system specified by a Moore machine and applies this technique to flight safety assessment and management, which is itself an emerging flight management automation aid.
Verification Guided Refinement of Flight Safety Assessment and Management System for Takeoff
Journal of Aerospace Information Systems ; 13 , 9 ; 357-369
2016-08-05
13 pages
Article (Journal)
Electronic Resource
English
Flight Safety Assessment and Management during Takeoff
AIAA | 2013
|Flight Safety Assessment and Management during Takeoff (AIAA 2013-4805)
British Library Conference Proceedings | 2013
|VSTOL autonomous takeoff flight control
AIAA | 1997
|