A framework for fault diagnosis of hybrid systems based on predicate abstractions

In this paper we aim at checking fault reconfigurability in hybrid systems. A hybrid system is a system mixing continuous and discrete behaviours that cannot be faithfully modeled neither by using a formalism with continuous dynamics only nor by a formalism including only discrete dynamics. We extend the well known framework of hybrid automata for modeling hybrid systems, adding faults leading to recoverable and unrecoverable states. We use a discrete abstraction of hybrid automata to design a diagnoser that observes the external behaviour of the system and announces whether a fault has occurred or not. Moreover if the diagnoser is able to detect the fault before the system reaches an unrecoverable state, then the automaton is also reconfigurable. We prove the effectiveness of this procedure with a simple case study.