Verification of the diagnosability of discrete-event systems in waters

Abstract

The task of detecting faults and reacting to them appropriately is a crucial aspect of a building a stable system. If a fault cannot be directly observed, its occurrence must be inferred from what can be observed. In the realm of discrete-event systems, the property of diagnosability has been defined, and several algorithms for testing diagnosability have been presented. Diagnosability relates to the ability for all possible faults to be correctly detected or inferred within a finite amount of time from their occurrence. WATERS (Waikato Analysis Toolkit for Events in Reactive Systems) is a software toolkit for the creation and analysis of discrete-event systems. In this report pre-existing existing algorithms for the verification of diagnosability and the implementation of one of these algorithms into WATERS are discussed. The created implementation can verify the diagnosability of a discrete-event system in polynomial time with respect to its state space and provide a counterexample if the discrete-event system was found to be not diagnosable.