Publications

Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction

Authors
Josť Vander Meulen, Charles Pecheur
Tags
, , , , , , ,
Title
Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction
Authors
Josť Vander Meulen, Charles Pecheur
 JVM_CP_NFM2011_TOOL.pdf Δ   351Kb   22 Feb 2011
Type
In Proceedings
Book title
NASA FORMAL METHODS 2011
Series
LNCS
Volume
6617
Publisher
Springer
Editor
Mihaela Bobaru, Klaus Havelund, Gerard Holzmann, Rajeev Joshi
Year
2011

Abstract

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 concurrents 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, Milestonese is able to translate a model into an equivalent Spin model or NuSMV model.

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.

Tags Tags: , , , , , , ,


BibTeX Record
  @INPROCEEDINGS{lvl-2011-2,
    TITLE = {Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order Reduction},
    AUTHOR = {Josť {Vander Meulen} and Charles Pecheur},
    YEAR = {2011},
    VOLUME = {6617},
    PUBLISHER = {Springer},
    EDITOR = {Mihaela Bobaru and Klaus Havelund and Gerard Holzmann and Rajeev Joshi},
    SERIES = {LNCS},
    URL = {http://lvl.info.ucl.ac.be/Publications/MilestonesAModelCheckerCombiningSymbolicModelCheckingAndPartialOrderReduction},
  }