Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL Properties
verfasst von : José Vander Meulen, Charles Pecheur
Erschienen in: NASA Formal Methods
Verlag: Springer Berlin Heidelberg
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
BDD-based 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 BDD-based techniques do not work well for loosely-synchronized models, whereas POR methods allow explicit-state model checkers to deal with large concurrent models. This paper presents an algorithm that combines symbolic model checking and POR to verify linear temporal logic properties without the next operator (LTL
X
), which performs better on models featuring asynchronous processes. Our algorithm adapts and combines three methods: Clarke et al.’s tableau-based symbolic LTL model checking, Iwashita et al.’s forward symbolic CTL model checking and Lerda et al.’s ImProviso symbolic reachability with POR. We present our approach, outline the proof of its correctness, and present a prototypal implementation and an evaluation on two examples.