Title: Formal verification of intermittent fault diagnosability of discrete-event systems using model-checking

Authors: Abderraouf Boussif; Mohamed Ghazel

Addresses: IFSTTAR, COSYS, ESTAS, Univ Lille Nord de France, F-59650 Villeneuve d'Ascq, France ' IFSTTAR, COSYS, ESTAS, Univ Lille Nord de France, F-59650 Villeneuve d'Ascq, France

Abstract: Fault diagnosis of complex and dynamic systems is a crucial and challenging task, essentially with respect to guaranteeing the reliable, safe and efficient operation of such systems. Most research in this field has been focused on permanent failure diagnosis, i.e., once a fault occurs, the system remains indefinitely faulty. However, experience with fault diagnosis in real-life systems shows that intermittent faults, i.e., faults that can be automatically recovered, are predominant and are among the most challenging kinds of faults to detect and isolate. In this paper, we address the formal verification of intermittent fault diagnosability in discrete-event systems. The system is modelled by a finite state automaton and intermittent faults are defined as faults that can automatically recover once they have occurred. Two definitions of diagnosability, regarding the detection of fault occurrence within a finite delay and the detection of fault occurrence before its recovery, are discussed. The diagnosability is analysed on the basis of the twin-plant structure, which is encoded as a Kripke structure, while diagnosability conditions are formulated using LTL temporal logic.

Keywords: discrete-event systems; fault diagnosis; diagnosability analysis; intermittent faults; model checking.

DOI: 10.1504/IJCCBS.2018.096192

International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.2, pp.193 - 213

Received: 11 Sep 2017
Accepted: 01 Jun 2018
Published online: 15 Nov 2018 *

Full-text access for editors Full-text access for subscribers Purchase this article Comment on this article