Symbolic Model Checking for Avionics
Radu I. Siminiceanu, Gianfranco Ciardo · Formal Methods for Industrial Critical Systems · 2012
For safety-critical avionics, regulatory authorities (the Federal Aviation Administration [FAA], the Civil Aeronautics Authority [CAA] or the Department of Defense [DoD]) require software development standards, such as MIL-STD-2167 for military systems and RTCA DO-178B for civil aircraft. This chapter presents the experience in applying the methodology (i.e., discrete-state model checking of abstracted models) to an industrial size application: the National Aeronautics and Space Administration (NASA) Runway Safety Monitor (RSM) software. The Integrated Display System (IDS) design enables RSM to exploit existing data communications facilities, displays, global positioning system (GPS), ground surveillance system information, and data links. Since most air safety incidents occur on or near runways, the RSM plays a key role in accident avoidance. RSM is not intended to prevent incursions, but to detect them and alert the pilots. RSM monitors traffic in a zone surrounding the runway where the takeoff or landing can occur. Controlled Vocabulary Terms airports; avionics; global positioning system