Model-Checking Based Fault Isolation in UML

We describe an approach to model-based fault isolation in large object oriented control systems. Our method relies on models of structure and behavior expressed in a subset of the Unified Modeling Language (UML). We consider system failures where on-line analysisis problematic, e.g. in safety-critical applications, leading to propagating alarms which have to be analyzed off-line. In our previous work we have shown how to use structural models, in the form of UML class diagrams, to reason about causal dependencies between error messages. In this paper we argue that models of behavior, in the form of UML state charts, together with verification techniques based on model checking further improve the ability to isolate faults off-line even when both models and observations are incomplete