Automatic Fault Localization for Property Checking

Goerschwin Fey; Stefan Simon Staber; Roderick Paul Bloem; Rolf Drechsler

doi:10.1109/TCAD.2008.923234

Automatic Fault Localization for Property Checking

Goerschwin Fey, Stefan Simon Staber, Roderick Paul Bloem, Rolf Drechsler

Institute of Applied Information Processing and Communications (7050)

Research output: Contribution to journal › Article › peer-review

Abstract

We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results

Original language	English
Pages (from-to)	1138-1149
Journal	IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Volume	27
Issue number	6
DOIs	https://doi.org/10.1109/TCAD.2008.923234
Publication status	Published - 2008

Access to Document

10.1109/TCAD.2008.923234

1 Finished

Formal Methods for Design & Verification
Jacobs, S., Bloem, R., Könighofer, R., Könighofer, B., Khalimov, A., Hofferek, G. & Braud-Santoni, N.
1/02/08 → 15/07/19
Project: Research area

Cite this

@article{4df6908d76ac4d5b9aa9f17849084e44,

title = "Automatic Fault Localization for Property Checking",

abstract = "We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results",

author = "Goerschwin Fey and Staber, {Stefan Simon} and Bloem, {Roderick Paul} and Rolf Drechsler",

year = "2008",

doi = "10.1109/TCAD.2008.923234",

language = "English",

volume = "27",

pages = "1138--1149",

journal = "IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems",

issn = "0278-0070",

publisher = "Institute of Electrical and Electronics Engineers",

number = "6",

}

TY - JOUR

T1 - Automatic Fault Localization for Property Checking

AU - Fey, Goerschwin

AU - Staber, Stefan Simon

AU - Bloem, Roderick Paul

AU - Drechsler, Rolf

PY - 2008

Y1 - 2008

N2 - We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results

AB - We present an efficient fully automatic approach to fault localization for safety properties stated in linear temporal logic. We view the failure as a contradiction between the specification and the actual behavior and look for components that explain this discrepancy. We find these components by solving the satisfiability of a propositional Boolean formula. We show how to construct this formula and how to extend it so that we find exactly those components that can be used to repair the circuit for a given set of counterexamples. Furthermore, we discuss how to efficiently solve the formula by using the proper decision heuristics and simulation-based preprocessing. We demonstrate the quality and efficiency of our approach by experimental results

U2 - 10.1109/TCAD.2008.923234

DO - 10.1109/TCAD.2008.923234

M3 - Article

VL - 27

SP - 1138

EP - 1149

JO - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

JF - IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems

SN - 0278-0070

IS - 6

ER -

Automatic Fault Localization for Property Checking

Abstract

Access to Document

Fingerprint

Projects

Formal Methods for Design & Verification

Cite this