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

Institut für Angewandte Informationsverarbeitung und Kommunikationstechnologie (7050)

Publikation: Beitrag in einer Fachzeitschrift › Artikel › Begutachtung

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

Originalsprache	englisch
Seiten (von - bis)	1138-1149
Fachzeitschrift	IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Jahrgang	27
Ausgabenummer	6
DOIs	https://doi.org/10.1109/TCAD.2008.923234
Publikationsstatus	Veröffentlicht - 2008

Zugriff auf Dokument

10.1109/TCAD.2008.923234

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
Projekt: Arbeitsgebiet

Dieses zitieren

@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 = "1937-4151",

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

SN - 1937-4151

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

IS - 6

ER -

Automatic Fault Localization for Property Checking

Abstract

Zugriff auf Dokument

Fingerprint

Projekte

Formal Methods for Design & Verification

Dieses zitieren