Name
Title | ||
|---|---|---|
Modular Model Checking of Large Asynchronous Designs with Efficient Abstraction Refinement |
Abstract | ||
|---|---|---|
Divide-and-conquer is essential to address state explosion in model checking. Verifying each individual component in a system, in isolation, efficiently requires an appropriate context, which traditionally is obtained by hand. This paper presents an efficient modular model checking approach for asynchronous design verification. It is equipped with a novel abstraction refinement method that can refine a component abstraction to be accurate enough for successful verification. It is fully automated, and eliminates the need of finding an accurate context when verifying each individual component, although such a context is still highly desirable. This method is also enhanced with additional state space reduction techniques. The experiments on several nontrivial asynchronous designs show that this method efficiently removes impossible behaviors from each component including ones violating correctness requirements. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1109/TC.2009.187 | IEEE Trans. Computers |
Keywords | Field | DocType |
abstraction,modular model checking,state-space methods,component abstraction,accurate context,model checking,novel abstraction refinement method,appropriate context,abstraction refinement,efficient abstraction refinement,logic verification,abstraction refinement method,additional state space reduction,accurate enough,state space reduction techniques,efficient modular model checking,asynchronous design verification,state explosion,modular verification,circuit verification,individual component,formal methods,formal verification,large asynchronous designs,refinement.,logic circuits,synchronization,cognition,computational modeling,informatics,data mining,divide and conquer,formal method,refinement | Abstraction model checking,Asynchronous communication,Synchronization,Programming language,Model checking,Computer science,Parallel computing,Correctness,Modular design,Formal methods,Distributed computing,Formal verification | Journal |
Volume | Issue | ISSN |
59 | 4 | 0018-9340 |
Citations | PageRank | References |
6 | 0.42 | 24 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Hao Zheng | 1 | 95 | 13.32 |
| Haiqiong Yao | 2 | 15 | 1.61 |
| Tomohiro Yoneda | 3 | 353 | 41.62 |