1999 | OriginalPaper | Buchkapitel
Partial Order Reduction in Presence of Rendez-vous Communications with Unless Constructs and Weak Fairness
verfasst von : Dragan Bošnački
Erschienen in: Theoretical and Practical Aspects of SPIN Model Checking
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.