Publications

Combining Partial Order Reduction with Symbolic Model Checking

Authors
José Vander Meulen
Tags
, , , , ,
Title
Combining Partial Order Reduction with Symbolic Model Checking
Authors
José Vander Meulen
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
Book
Volume
370
Publisher
Doctoral thesis, Université catholique de Louvain
Year
2012

Abstract

Model checking is an efficient technique for verifying properties on asynchronous systems. Unfortunately, it suffers from the so-called combinatorial state-space explosion problem. Two common approaches are used to fight this problem, with different perspectives. On the one hand, partial-order reduction (POR) methods explore a reduced state space in a property-preserving way. On the other hand, symbolic techniques use efficient structures such as binary decision diagrams (BDD's) to concisely encode and compute large state spaces. This thesis presents algorithms which, one way or another, combine symbolic model checking and partial-order reduction, allowing efficient verification of CTLX and LTLX properties on models featuring asynchronous processes.

At the root of our work was the ImProviso algorithm for computing reachable states, which combines POR and symbolic verification, and the FwdUntil method that supports verification of a subset of CTL. We present the PartialExploration algorithm which adapts and extends ImProviso to support the verification of a fragment of CTLX. Then, the evalCTLX algorithm merges the PartialExploration algorithm with the classical backward algorithm to support the totality of CTL.

The evalLTLX algorithm checks LTLX properties. We start from the tableau-based reduction of LTL verification of Clarke et al. which translates an LTL problem into a fair path detection problem. While classical BDD-based model-checking would perform this search with a backward traversal, we use the forward-traversal approach of Iwashita et al. Part of the resulting computation amounts to computing the reachable state space; to that end we use our PartialExploration algorithm.

The BPE algorithm adapts our PartialExploration algorithm and bounded model checking techniques in an original way. The encoding to a SAT problem strongly reduces the complexity and non-determinism of each transition step, allowing efficient analysis even with longer execution traces.

The algorithms developed in this thesis were implemented in a new model checker which is called Milestones. It allows us to check the absence of deadlock, LTL properties, and CTL properties. In order to compare our approach to others, Milestones can translate a model into an equivalent Spin model or NuSMV model.

Tags Tags: , , , , ,

BibTeX Record
  @BOOK{lvl-2012-971829,
    TITLE = {Combining Partial Order Reduction with Symbolic Model Checking},
    AUTHOR = {José {Vander Meulen}},
    YEAR = {2012},
    VOLUME = {370},
    PUBLISHER = {Doctoral thesis, Université catholique de Louvain},
    URL = {https://lvl.info.ucl.ac.be/Publications/CombiningPartialOrderReductionWithSymbolicModelChecking},
  }