Diagnosing hybrid cyber-physical systems using state-space models and satisfiability modulo theory

Diagnosing faults in large cyber-physical production systems is hard and often done manually. n this paper we present an approach to leverage methods from the fault detection and isolation community as well as model-based diagnosis to diagnose faults. Given a model of the production system we capture its dynamic behaviour with a state-space model. Then we translate the state-space model into satisfiability theory modulo linear arithmetic over reals. This translation converts numerical information in symbolic logic. These symbols can be used to diagnose faults with Reiter's diagnosis algorithm. We use a four-tank model as a demonstration use case. Under the assumption that the use-case is fully-observable (i.e. all components except the water tanks can be observed) our methodology detects all injected faults.