Java']Java2CSP-A Model-Based Diagnosis Tool Not Only for Software Debugging

Model-based reasoning has been an active research area for several decades providing foundations for fault detection, localization, and repair not only in the context of system and hardware diagnosis but also in localizing software bugs. Java2CSP allows for mapping Java-like programs into a corresponding constraint representation. The constraint representation makes use of a health state variable indicating whether a certain statement is correct or faulty. A constraint solver can be used for computing diagnoses for a given failing test case. In this paper, we present the tool and also show how more classical diagnosis problems can be directly mapped to their program representation, which allows to use Java2CSP in different settings, including teaching model-based diagnosis.