SMT-based Diagnosability Analysis of Real-Time Systems

Fault diagnosis is a crucial and challenging task in the automatic control of complex systems, whose efficiency depends on a system property called diagnosability. Diagnosability describes the capability of a system to determine with certainty whether a fault has effectively occurred based on a sequence of observations. The diagnosability problem of discrete event systems has received considerable attention in the literature. However, up to now little work takes into account explicit time constraints during this analysis, which are however naturally present in real-life systems and thus cannot be neglected considering their impact on this property. In this paper, we first rephrase diagnosability definition for timed automata before showing the impact of time constraints on this property. Then we propose a new SMT-based approach to verify bounded time diagnosability on timed automata. The idea is to encode the sufficient and necessary condition for diagnosability in SMT. Finally, the experimental results are presented to show the efficiency of the SMT-based paradigm. (C) 2018, IFAC (International Federation of Automatic Control) Hosting by Elsevier Ltd. All rights reserved.