Application of temporal logic for safety supervisory control and model-based hazard monitoring

- We apply Temporal Logic (TL) for safety supervisory control and hazard monitoring.
- The verification of safety properties expressed in TL supports safety interventions.
- This capability is illustrated through a runway overrun case study.
- TL safety constraints and hazard metrics are proposed for the analyzed system.

In this work, we extend a previously introduced framework for safety supervisory control with the ingredient of Temporal Logic (TL) to improve both accident prevention and dynamic risk assessment. We examine the synergies obtained from integrating model-based hazard modeling/monitoring with the verification of safety properties expressed in TL. This expanded framework leverages tools and ideas from Control Theory and Computer Science, and is meant to guide safety intervention both on-line and off-line, either during the design stages or during operation to support operator's situational awareness and decision-making in the face of emerging hazardous situations. We illustrate these capabilities and the insight that results from the integration of the proposed ingredients through a detailed case study. The study involves a runway overrun by a business jet, and it shows how hardware, software, and operators' control actions and responses can be integrated within the proposed framework. The aircraft suffered from a faulty logic in the Full Authority Digital Engine Computer (FADEC), which prevented the pilot from activating the thrust reversers in a particular operational scenario. We examine the accident sequence against three system safety principles expressed in TL: the fail-safe principle, the defense-in-depth principle, and the observability-in-depth principle. The framework is implemented in Simulink and Stateflow, and is shown to provide important feedback for dynamic risk assessment and accident prevention. When applied on-line, it provides warning signs to support the sensemaking of emerging hazardous situations, and identifying adverse conditions that are closer to being released. When applied off-line, it provides diagnostic information regarding missing or inadequate safety features embedded in the system. For the specific case study, we propose a new TL safety constraint (based on speed measurements and the history of pressure sensors from the landing gears) to be incorporated in this and other aircraft FADEC, and that could have prevented the hazardous situation, in this case a rejected takeoff following tire explosion, from turning into a deadly accident. We conclude with some recommendations to prevent similar accident recurrences and to improve accident prevention.