Publications

PyNuSMV: NuSMV as a Python Library

Authors
Simon Busard, Charles Pecheur
Tags
, , ,
Title
PyNuSMV: NuSMV as a Python Library
Authors
Simon Busard, 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 2013
Series
LNCS
Volume
7871
Pages
453-458
Publisher
Springer-Verlag
Editor
G. Brat, N. Rungta, and A. Venet
Year
2013

Abstract

NuSMV is a state-of-the-art model checker providing BDD- based and SAT-based techniques and a rich modeling language. While the tool is powerful, it is hard to customize it because of the size and complexity of its code base (more than 200K LOC). This paper presents PyNuSMV, a Python framework for prototyping and experimenting with BDD-based model-checking algorithms based on NuSMV.

PyNuSMV provides a rich and flexible programmable platform to implement new logics and experiment with custom model-checking algorithms. Thanks to PyNuSMV, it is possible to use NuSMV functionalities without understanding its whole code base or struggling with implementation details such as memory management. PyNuSMV has already been used to implement model-checking algorithms for rich logics such as ARCTL and CTLK.

This paper describes the structure and usage of PyNuSMV, illustrates its use by re-implementing CTL model checking, and reports initial per- formance results showing negligible impact compared to native NuSMV.

Tags Tags: , , ,

BibTeX Record
  @INPROCEEDINGS{lvl-2013-707009,
    TITLE = {PyNuSMV: NuSMV as a Python Library},
    AUTHOR = {Simon Busard and Charles Pecheur},
    YEAR = {2013},
    VOLUME = {7871},
    PAGES =  {453-458},
    PUBLISHER = {Springer-Verlag},
    EDITOR = {G. Brat and N. Rungta and and A. Venet},
    SERIES = {LNCS},
    URL = {https://lvl.info.ucl.ac.be/Publications/PyNuSMVNuSMVAsAPythonLibrary},
  }