A jointree algorithm for diagnosability and its application to the verification of distributed software systems
Anika Schumann, Wolfgang Mayer, Markus Stumptner · 2008
Diagnosability is an essential property that deter-mines how accurate any diagnostic reasoning can be on a system. While diagnosability in a discrete event system can be decided by synchronising finite state machines representing ambiguous paths in in-dividual subsystems, this synchronisation operation remains prohibitively complex. We propose a novel algorithm that exploits structure and locality properties of a system to avoid expen-sive synchronisation operations. By propagating concise summary information reflecting diagnos-ability of small subsystems, diagnosability of the entire system is computed incrementally. As a re-sult, we obtain an efficient algorithm that can not only decide (non)diagnosability but that is also ap-plicable in scenarios where computational resources are limited. We also show how our algorithm can be applied to analyse distributed (software) systems. 1