Name
Title | ||
|---|---|---|
Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness |
Abstract | ||
|---|---|---|
If synchronizing (rendez-vous) communications are used in the Promela models, the unless construct and the weak fairness algorithm are not compatible with the partial order reduction algorithm used in Spin's verifier. After identifying the wrong partial order reduction pattern that causes the incompatibility, we give solutions for these two problems. To this end we propose corrections in the identification of the safe statements for partial order reduction and as an alternative, we discuss corrections of the partial order reduction algorithm. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48234-2_4 | SPIN |
Keywords | Field | DocType |
partial order reduction,partial order reduction algorithm,promela model,safe statement,weak fairness,weak fairness algorithm,rendez-vous communications,wrong partial order reduction | Spin-½,Computer science,Synchronizing,Algorithm,Real-time operating system,Promela,Partial order reduction,Partially ordered set | Conference |
Volume | ISSN | ISBN |
1680 | 0302-9743 | 3-540-66499-8 |
Citations | PageRank | References |
4 | 0.44 | 11 |
Authors | ||
1 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Dragan Bosnacki | 1 | 276 | 26.95 |