Name
Abstract | ||
|---|---|---|
Despite significant research on state-space reductions, the poor scalability of model checking for reasoning about behavioral models of large, complex systems remains the chief obstacle to its broad acceptance. One strategy for making further progress is to exploit characteristics of classes of systems to develop domain-specific reductions. In this paper, we identify a structural property of system state-spaces, which we call quasi-cyclic structure, that can be leveraged to significantly reduce the space requirements of model checking. We give a formal characterization of quasi-cyclic state-spaces and describe a state-space exploration algorithm for exploiting that structure. In addition, we describe a class of real-time embedded systems that are quasi-cyclic, we outline how we customized an existing model checking framework to implement space-efficient search of quasi-cyclic systems, and we present experimental data that demonstrate multiple orders of magnitude reductions in space consumption. |
Year | DOI | Venue |
|---|---|---|
2003 | 10.1007/978-3-540-45212-6_12 | Lecture Notes in Computer Science |
Keywords | Field | DocType |
model checking,complex system,state space | Complex system,Obstacle,Model checking,Computer science,Exploit,Real-time operating system,Software development,Distributed computing,Scalability | Conference |
Volume | ISSN | Citations |
2855 | 0302-9743 | 10 |
PageRank | References | Authors |
0.98 | 11 | 4 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Matthew Dwyer | 1 | 3998 | 289.30 |
| Non Robby | 2 | 10 | 0.98 |
| Xianghua Deng | 3 | 170 | 11.13 |
| John Hatcliff | 4 | 2373 | 212.83 |