Anzeige
Erschienen in:
2011 | OriginalPaper | Buchkapitel
Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction
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
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.