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.
International Journal of Critical Computer-Based Systems, 2018 Vol.8 No.2, pp.193 - 213
Available online: 09 Nov 2018 *Full-text access for editors Access for subscribers Purchase this article Comment on this article