Back to Search
Start Over
Using Abstraction to Guide the Search for Long Error Traces.
- Source :
-
IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems . Mar2013, Vol. 32 Issue 3, p453-466. 14p. - Publication Year :
- 2013
-
Abstract
- Model checking is a formal method for verifying whether the system satisfies a user-defined specification. Compared to simulation, model checking is restricted in capacity. On the other hand, simulation is weak in detecting bugs that require long and complex sequences of events to be exposed. This paper combines model checking and simulation in an abstraction-refinement scheme to mitigate the problems of both methods. Abstraction refinement iteratively constructs a simplified model to verify the original model. While a simplified model mitigates the weakness of model checking, the set of simplified error traces model helps guide simulation toward deep bugs. In abstraction refinement, concretization—a process of deriving an error trace in the original model from the abstract ones—is used to invalidate spurious abstract error traces or to refute a property. In this paper, we describe a novel concretization algorithm that combines simulation with satisfiability to efficiently refute properties with very long error traces. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISSN :
- 02780070
- Volume :
- 32
- Issue :
- 3
- Database :
- Academic Search Index
- Journal :
- IEEE Transactions on Computer-Aided Design of Integrated Circuits & Systems
- Publication Type :
- Academic Journal
- Accession number :
- 85705421
- Full Text :
- https://doi.org/10.1109/TCAD.2012.2228266