Formally expressing the semantics of observer-based fault detection software

TL;DR

This paper develops a formal framework to specify and verify observer-based fault detection software for safety-critical systems, enhancing reliability through automatic verification of high-level properties.

Contribution

It introduces a formal language for expressing fault detection properties and integrates these annotations into software for automatic verification, improving software reliability.

Findings

All tested methods detect faults acceptably in experiments.

Formal annotations enable automatic verification of fault detection properties.

Enhances reliability of fault detection software in safety-critical systems.

Abstract

The aim is to create reliable and verifiable fault detection software to detect abrupt changes in safety-critical dynamic systems. Fault detection methods are implemented as software on digital computers that monitor and control the system. We implement three observer-based fault detection methods on a 3 degrees of freedom (3DOF) laboratory helicopter, in the form of software. We examine the performance of those methods to detect different faults during flight in a closed-loop setup. All selected methods show acceptable detection performance. However, it is not possible to repeat the test for every possible conditions, inputs and fault scenarios. In this paper, we translate fault detection properties and mathematical proofs into a formal language, previously used in software validation and verification. We include the translated properties in software in the form of non-executable annotations that can be read by machine. Consequently, some high level functional properties of the code can be verified by automatic software verification tools. This certifies fault detection software for a set of bounded data and increases the reliability in practice.