Diagnosability Behaviour over faulty concurrent systems

Complex systems often exhibit unexpected faults that are difficult to handle. It is desirable that such systems are diagnosable, i.e. faults are automatically detected as they occur (or shortly afterwards), enabling the system to handle the fault or recover. Formally, a system is diagnosable if it is possible to detect every fault, in a finite time after they occurred, by only observing available information from the system. Complex systems are usually built from simpler subsystems running concurrently. In order to model different communication and synchronization methods, the interactions between subsystems may be specified in various ways. In this work we present an analysis of the di-agnosability problem in concurrent systems under such different interaction strategies, with arbitrary faults occurring freely in subsystems. We rigorously define diagnosability in this setting, and formally prove in which cases diagnosability is preserved under composition. We illustrate our approach with several examples, and present a tool that implements our analysis.