Testing and model-checking techniques for diagnosis

M. Gromov, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

4 Citations (Scopus)
81 Downloads (Pure)


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 diagnostic 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 characterise 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 procedures for diagnostic testing.
Original languageEnglish
Title of host publicationProceedings of the 19th IFIP TC6/WG6.1 International Conference on Testing of Software and Communicating Systems (TestCom 2007) & 7th International Workshop on Formal Approaches to Testing of Software (FATES 2007) 26-29 June 2007, Tallinn, Estonia
EditorsA. Petrenko, M. Veanes, J. Tretmans, W. Grieskamp
Place of PublicationBerlin, Germany
ISBN (Print)978-3-540-73065-1
Publication statusPublished - 2007
Eventconference; TestCom 2007 & FATES 2007, Tallinn, Estonia; 2007-06-26; 2007-06-29 -
Duration: 26 Jun 200729 Jun 2007

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conferenceconference; TestCom 2007 & FATES 2007, Tallinn, Estonia; 2007-06-26; 2007-06-29
OtherTestCom 2007 & FATES 2007, Tallinn, Estonia


Dive into the research topics of 'Testing and model-checking techniques for diagnosis'. Together they form a unique fingerprint.

Cite this