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
FM2018 Δ   0Kb   28 May 2020
Fmics2013 Δ   0Kb   28 May 2020
GandALF2017 Δ   0Kb   28 May 2020
HMI2011 Δ   0Kb   28 May 2020
LVLPrivate Δ   0Kb   28 May 2020
LVLPrivateNews Δ   0Kb   28 May 2020
Main Δ   0Kb   28 May 2020
Members Δ   0Kb   28 May 2020
Publications Δ   4Kb   28 May 2020
Site Δ   0Kb   28 May 2020
Talks Δ   4Kb   28 May 2020
Tools Δ   0Kb   28 May 2020
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 = {https://lvl.info.ucl.ac.be/Publications/MilestonesAModelCheckerCombiningSymbolicModelCheckingAndPartialOrderReduction},
  }