Name
Title | ||
|---|---|---|
Milestones: a model checker combining symbolic model checking and partial order reduction |
Abstract | ||
|---|---|---|
Symbolic techniques and partial order reduction (POR) are two fruitful approaches to deal with the combinatorial explosion of model checking. Unfortunately, past experience has shown that symbolic techniques do not work well for loosely-synchronized models, whereas, by applying POR methods, explicit-state model checkers are able to deal with large concurrent models. This paper presents the Milestones model checker which combines symbolic techniques and POR. Its goal is to verify temporal properties on concurrent systems. On such a system, Milestones allows to check the absence of deadlock, LTL properties, and CTL properties. In order to compare our approach to others, Milestones is able to translate a model into an equivalent Spin model [7] or NuSMV model [4]. We briefly present the theoretical foundation on which Milestones is based on. Then, we present the Milestones model checker, and an evaluation based on an example. |
Year | Venue | Keywords |
|---|---|---|
2011 | NASA Formal Methods | partial order reduction,large concurrent model,equivalent spin model,explicit-state model checker,milestones model checker,concurrent system,por method,symbolic technique,model checking,loosely-synchronized model,symbolic model checking,nusmv model |
Field | DocType | Volume |
Programming language,Model checking,Computer science,Deadlock,Binary decision diagram,Theoretical computer science,Partial order reduction,Spin model,Milestone (project management),Combinatorial explosion,Symbolic trajectory evaluation | Conference | 6617 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
11 | 2 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| José Vander Meulen | 1 | 6 | 1.57 |
| Charles Pecheur | 2 | 284 | 28.50 |