A Fast Approach of Locating Complex System Design Errors

Zhi Yuan Chen; Shao Bin Huang; Li Li Han

doi:10.4028/www.scientific.net/KEM.572.115

Paper Titles

Development of an Online System for Recycling Consumer Electronic Products Using the Internet, NFC and RFID Technologies
p.90

Information Flows and Design Intent in the Core of Future Product-Services in the Field of Manufacturing Industry
p.103

Framework of Man-Machine-Environment Application System Engineering throughout Life Cycle of Large Scale Vessel
p.107

Formalization of Reconfigurable Mechanisms in Task Based Conceptual Design Method
p.111

A Fast Approach of Locating Complex System Design Errors
p.115

Coordination of Design Processes in Two Perspectives of Computer Aided Design
p.119

Application of Baseline in Configuration Management for Aerospace Product Design
p.123

An Ontology-Based Framework for Ergonomics Knowledge Classification and Representation
p.127

A Design of an Optical System of Liquid Filled Lens which can Adjust the Focus
p.131

HomeKey Engineering MaterialsKey Engineering Materials Vol. 572A Fast Approach of Locating Complex System Design...

A Fast Approach of Locating Complex System Design Errors

Abstract:

Model checking technique can give a specific counterexample which explains how the system violates some assertion when model does not satisfy the specification. However, it is a tedious work to understand the long counterexamples. We propose a genetic algorithm to enhance the efficiency of understanding long counterexample by computing the minimal unsatisfiable subformula. Besides, we also propose a Craig interpolation computation-based method to understand counterexample. The causes which are responsible for model failure are extracted by deriving interpolation from the proof of the nonsatisfiability of the initial state and the weakest precondition of counterexample. Experimental results show that our methods improve the efficiency of understanding counterexamples and debugging significantly.

You might also be interested in these eBooks

View Preview

Info:

Periodical:

Key Engineering Materials (Volume 572)

Pages:

115-118

DOI:

https://doi.org/10.4028/www.scientific.net/KEM.572.115

Citation:

Cite this paper

Online since:

September 2013

Authors:

Zhi Yuan Chen, Shao Bin Huang, Li Li Han

Keywords:

Craig Interpolation, Minimal Unsatisfiable Subformula, Model Checking, Understanding Counterexample

Export:

RIS, BibTeX

Price:

Permissions CCC:

Request Permissions

Permissions PLS:

Request Permissions

Сopyright:

Citation:

References

[1] E Clarke, E Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. Logics of Programs, 1982, pp.52-71.

DOI: 10.1007/bfb0025774

Google Scholar

[2] I Beer, S Ben-David, H Chockler, et al. Explaining counterexamples using causality /Computer Aided Verification. 2009, pp.94-108.

DOI: 10.1007/978-3-642-02658-4_11

Google Scholar

[3] M Jose, R Majumdar. Cause Clue Clauses: Error Localization using Maximum Satisfiability. Arxiv preprint arXiv: 1011. 1589, (2010).

DOI: 10.1145/2345156.1993550

Google Scholar

[4] HUANG Hongtao, HUANG Shaobin, CHEN Zhiyuan and ZHANG Tao. Understanding Counterexamples Based on Craig Interpolation. Journal of Jilin University (Science Edition), 2013, 53(1), pp.94-100.

Google Scholar