Testing and Model-Checking Techniques for Diagnosis

Abstract. Black-box testing is a popular technique for assessing the quality of a system. However, in case of a test failure, only little information is available to identify the root-cause of the test failure. In such cases, additional diagnostic tests may help. We present techniques and a methodology for efficiently conducting di-agnostic tests based on explicit fault models. For this, we rely on Model-Based Testing techniques for Labelled Transition Systems. Our techniques rely on, and exploit differences in outputs (or inputs) in fault models, respectively. We char-acterise the underlying concepts for our techniques both in terms of mathematics and in terms of the modal µ-calculus, which is a powerful temporal logic. The latter characterisations permit the use of efficient, off-the-shelf model checking techniques, leading to provably correct algorithms and pseudo decision proce-dures for diagnostic testing.