Publications

Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties

Authors
Josť Vander Meulen, Charles Pecheur
Tags
, , , ,
Title
Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties
Authors
Josť Vander Meulen, Charles Pecheur
 JVM_CP_NFM_2011_REGULAR.pdf Δ   459Kb   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

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, by applying POR methods, explicit-state model checkers are able to deal with large concurrent models. This paper presents an algorithm which combines symbolic model checking and POR to verify linear temporal logic properties (LTL without the next time operator) which performs better on models featuring asynchronous processes. Our algorithm adapts and combines three methods: Lerda et al.'s ImProviso algorithm which incorporates POR in symbolic model checking, Iwashita et al.'s forward symbolic CTL model checking, and Clarke et al.'s symbolic LTL model checking algorithm. We present our algorithm, outline the proof of its correctness, and present a prototypal implementation and an evaluation on two examples.

Tags Tags: , , , ,


BibTeX Record
  @INPROCEEDINGS{lvl-2011-1,
    TITLE = {Combining Partial Order Reduction and Symbolic Model Checking to verify LTL properties},
    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/CombiningPartialOrderReductionAndSymbolicModelCheckingToVerifyLTLProperties},
  }