More Web Proxy on the site http://driver.im/

Article

Finding and fixing faults

Authors:

Barbara Jobstmann,

Roderick BloemAuthors Info & Claims

CHARME'05: Proceedings of the 13 IFIP WG 10.5 international conference on Correct Hardware Design and Verification Methods

Pages 35 - 49

https://doi.org/10.1007/11560548_6

Published: 03 October 2005 Publication History

Abstract

We present a method for combined fault localization and correction for sequential systems. We assume that the specification is given in linear-time temporal logic and state the localization and correction problem as a game that is won if there is a correction that is valid for all possible inputs. For invariants, our method guarantees that a correction is found if one exists. The set of fault models we consider is very general: components can be replaced by arbitrary new functions. We compare our approach to model based diagnosis and show that it is more precise. We present experimental data that supports the applicability of our approach, obtained from a symbolic implementation of the algorithm in the Vis model checker.

References

[1]

R. K. Brayton et al. VIS: A system for verification and synthesis. In T. Henzinger and R. Alur, editors, Eighth Conference on Computer Aided Verification (CAV'96), pages 428-432. Springer-Verlag, Rutgers University, 1996. LNCS 1102.

Digital Library

[2]

T. Ball, M. Naik, and S. K. Rajamani. From symptom to cause: Localizing errors in counterexample traces. In 30th Symposium on Principles of Programming Languages (POPL 2003), pages 97-105, January 2003.

Digital Library

[3]

L. Console, G. Friedrich, and D. Theseider Dupré. Model-based diagnosis meets error diagnosis in logic programs. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI'93), pages 1494-1499. Morgan-Kaufmann, 1993.

[4]

E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.

Digital Library

[5]

L. Console and P. Torasso. A spectrum of logical definitions of model-based diagnosis. Computational Intelligence, 7(3):133-141, 1991.

Digital Library

[6]

P.-Y. Chung, Y.-M. Wang, and I. N. Hajj. Logic design error diagnosis and correction. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 2:320- 332, 1994.

Digital Library

[7]

M. Fahim Ali, A. Veneris, S. Safarpur, R. Drechsler, A. Smith, and M. Abadir. Debugging sequential circuits using boolean satisfiability. In International Conference on Computer Aided Design, pages 204-209, 2004.

Digital Library

[8]

A. Groce. Error explanation with distance metrics. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), pages 108-122, Barcelona, Spain, March-April 2004. LNCS 2988.

[9]

A. Groce and W. Visser. What went wrong: Explaining counterexamples. In Model Checking of Software: 10th International SPIN Workshop, pages 121-135. Springer-Verlag, May 2003. LNCS 2648.

Digital Library

[10]

W. Hamscher and R. Davis. Diagnosing circuits with state: An inherently underconstrained problem. In Proceedings of the Fourth National Conference on Artificial Intelligence (AAAI'84), pages 142-147, Austin, TX, 1984.

[11]

B. Jobstmann, A. Griesmayer, and R. Bloem. Program repair as a game. To appear at Computer Aided Verification, 2005.

Digital Library

[12]

H. Jin, K. Ravi, and F. Somenzi. Fate and free will in error traces. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'02), pages 445-459, Grenoble, France, April 2002. LNCS 2280.

Digital Library

[13]

J. de Kleer and B. C. Williams. Diagnosing multiple faults. Artificial Intelligence, 32:97-130, 1987.

Digital Library

[14]

H.-T. Liaw, J.-H. Tsiah, and I. N. Hajj. Efficient automatic diagnosis of digital circuits. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 464-467, 1990.

[15]

J. C. Madre, O. Coudert, and J. P. Billon. Automating the diagmosis and the rectification of design error with PRIAM. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 30-33, 1989.

[16]

D. L. Poole, R. Goebel, and R. Aleliunas. Theorist: a logical reasoning system for defaults and diagnosis. In N. Cercone and G. McCalla, editors, The Knowledge Frontier: Essays in the Representation of Knowledge, pages 331-352. Springer Verlag, 1987.

[17]

R. Reiter. A theory of diagnosis from first principles. Artificial Intelligence, 32:57- 95, 1987.

Digital Library

[18]

M. Renieris and S. P. Reiss. Fault localization with nearest neighbor queries. In International Conference on Automated Software Engineering, pages 30-39, Montreal, Canada, October 2003.

[19]

K. Ravi and F. Somenzi. Minimal assignments for bounded model checking. In International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS'04), pages 31-45, Barcelona, Spain, March-April 2004. LNCS 2988.

[20]

M. Stumptner and F.Wotawa. Debugging functional programs. In Proceedings on the 16th International Joint Conference on Artificial Intelligence, 1999.

Digital Library

[21]

M. Tomita, T. Yamamoto, F. Sumikawa, and K. Hirano. Rectification of multiple logic design errors in multiple output circuits. In Proceedings of the Design Automation Conference, pages 212-217, 1994.

Digital Library

[22]

M. Vardi and P. Wolper. Reasoning about infinite computations. Information and Computation, 115:1-37, 1994.

Digital Library

[23]

A. Wahba and D. Borrione. Design error diagnosis in sequential circuits. In Correct Hardware Design and Verification Methods (CHARME'95), pages 171-188, 1995. LNCS 987.

Digital Library

[24]

A. Zeller. Isolating cause-effect chains from computer programs. In 10th International Symposium on the Foundations of Software Engineering (FSE-10), pages 1-10, November 2002.

Digital Library

[25]

A. Zeller and R. Hildebrandt. Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering, 28(2):183-200, February 2002.

Digital Library

Cited By

Ahmad HHuang YWeimer WFalsafi BFerdman MLu SWenisch T(2022)CirFix: automatically repairing defects in hardware design codeProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507763(990-1003)Online publication date: 28-Feb-2022
https://dl.acm.org/doi/10.1145/3503222.3507763
Santolucito MWinograd-Cort DGiavitto J(2021)Human-in-the-loop program synthesis for live codingProceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3471872.3472972(47-53)Online publication date: 27-Aug-2021
https://dl.acm.org/doi/10.1145/3471872.3472972
Gazzola LMicucci DMariani L(2019)Automatic Software RepairIEEE Transactions on Software Engineering10.1109/TSE.2017.275501345:1(34-67)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1109/TSE.2017.2755013
Show More Cited By

Finding and fixing faults
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
      1. Software defect analysis
  2. Software organization and properties
    1. Software functional properties
      1. Formal methods

Recommendations

Finding Faults

The injection of an error can, in fact, cause the leakage of confidential information. Often, the only way to attack strong cryptographic implementations is to attack the infrastructure upon which they are built. This infrastructure is most often the ...
Finding and fixing faults

Knowing that a program has a bug is good, knowing its location is better, but a fix is best. We present a method to automatically locate and correct faults in a finite state system, either at the gate level or at the source level. We assume that the ...
On undetectable faults and fault diagnosis

The presence of an undetectable fault u_i may modify the response of a detectable fault d_j to a test set used for fault diagnosis. This may impact the accuracy of fault diagnosis based on the responses of single faults. Many state-of-the-art diagnosis ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

CHARME'05: Proceedings of the 13 IFIP WG 10.5 international conference on Correct Hardware Design and Verification Methods

October 2005

408 pages

ISBN:3540291059

Editors:
Dominique Borrione
TIMA Laboratory, VDS Group, Grenoble, France
,
Wolfgang Paul
Computer Science Dept., Saarland University, Saarbrücken, Germany

Sponsors

INTEL: Intel Corporation
Infineon Technologies AG: Infineon Technologies AG
IBM Corporation

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 03 October 2005

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

30
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ahmad HHuang YWeimer WFalsafi BFerdman MLu SWenisch T(2022)CirFix: automatically repairing defects in hardware design codeProceedings of the 27th ACM International Conference on Architectural Support for Programming Languages and Operating Systems10.1145/3503222.3507763(990-1003)Online publication date: 28-Feb-2022
https://dl.acm.org/doi/10.1145/3503222.3507763
Santolucito MWinograd-Cort DGiavitto J(2021)Human-in-the-loop program synthesis for live codingProceedings of the 9th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design10.1145/3471872.3472972(47-53)Online publication date: 27-Aug-2021
https://dl.acm.org/doi/10.1145/3471872.3472972
Gazzola LMicucci DMariani L(2019)Automatic Software RepairIEEE Transactions on Software Engineering10.1109/TSE.2017.275501345:1(34-67)Online publication date: 1-Jan-2019
https://dl.acm.org/doi/10.1109/TSE.2017.2755013
Gulwani SRadiček IZuleger F(2018)Automated clustering and program repair for introductory programming assignmentsACM SIGPLAN Notices10.1145/3296979.319238753:4(465-480)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192387
Wang KSingh RSu Z(2018)Search, align, and repair: data-driven feedback generation for introductory programming exercisesACM SIGPLAN Notices10.1145/3296979.319238453:4(481-495)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192384
Gulwani SRadiček IZuleger FFoster JGrossman D(2018)Automated clustering and program repair for introductory programming assignmentsProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192387(465-480)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192387
Wang KSingh RSu ZFoster JGrossman D(2018)Search, align, and repair: data-driven feedback generation for introductory programming exercisesProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192384(481-495)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192384
Zemín LBrida SGodio ACornejo CDegiovanni RRegis GAguirre NFrias MGaleotti JPetke J(2017)An analysis of the suitability of test-based patch acceptance criteriaProceedings of the 10th International Workshop on Search-Based Software Testing10.5555/3105427.3105431(14-20)Online publication date: 20-May-2017
https://dl.acm.org/doi/10.5555/3105427.3105431
Attie PBab KSakr M(2017)Model and Program Repair via SAT SolvingACM Transactions on Embedded Computing Systems10.1145/314742617:2(1-25)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3147426
(2015)Model and program repair via SAT solvingProceedings of the 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign10.1109/MEMCOD.2015.7340481(148-157)Online publication date: 1-Sep-2015
https://dl.acm.org/doi/10.1109/MEMCOD.2015.7340481
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents