We found a match
Your institution may have access to this item. Find your institution then sign in to continue.
- Title
Fault localization using a model checker.
- Authors
Griesmayer, Andreas; Staber, Stefan; Bloem, Roderick
- Abstract
If a program does not fulfill its specification, a model checker can deliver a counterexample. However, although such a counterexample shows how the specification can be violated, it typically comprises large parts of the program and gives little information about which of the visited statements is responsible for the error. In this article, we show that model checkers can also be used to perform model-based diagnosis and thus fault localization. The approach leads to significantly more precise diagnoses than the state-of-the-art and typically rules out 90–99% of the code as possible fault locations. The approach is general and can be applied to any system that is amenable to model checking (with respect to language and complexity). To demonstrate the applicability and high precision of our approach, we present implementations for C programs using two different model checking tools and show experimental results from the TCAS case study and an integration with the DDVerify framework to debug Linux device drivers. Copyright © 2009 John Wiley & Sons, Ltd.
- Subjects
LOCALIZATION theory; COMPUTER software; PROGRAMMING languages; CASE studies; LINUX device drivers (Computer programs)
- Publication
Software Testing: Verification & Reliability, 2010, Vol 20, Issue 2, p149
- ISSN
0960-0833
- Publication type
Article
- DOI
10.1002/stvr.421