Name
Abstract | ||
|---|---|---|
Partial order reduction has been very successful at combatting the state explosion problem for lower-level formalisms, but has thus far made hardly any impact for model checking higher-level formalisms such as B, Z or TLA+. This paper attempts to remedy this issue in the context of Event-B, with its much more fine-grained events and thus increased potential for event-independence and partial order reduction. In this work, we provide a detailed description of a partial order reduction for explicit state model checking in ProB. The technique is evaluated on a variety of models. The implementation of the method is discussed, which is based on new constraint-based analyses. Further, we give a comprehensive description for elaborating the implementation into the LTL model checker of ProB for checking LTL¿X formulae. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/s00165-015-0351-1 | Formal Aspects of Computing |
Keywords | Field | DocType |
Model checking, Partial order reduction, Static analysis, Event-B, LTL | Discrete mathematics,Model checking,Computer science,Static analysis,Theoretical computer science,State model,Partial order reduction,Rotation formalisms in three dimensions | Journal |
Volume | Issue | ISSN |
28 | 2 | 1433-299X |
Citations | PageRank | References |
1 | 0.35 | 25 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ivaylo Dobrikov | 1 | 4 | 1.81 |
| Michael Leuschel | 2 | 2156 | 135.89 |