PyNuSMV: NuSMV as a Python Library

Busard, Simon;Pecheur, Charles
(2013) 5th NASA Formal Methods Symposium (NFM 2013) — Location: NASA Ames Research Center, Moffett Field, CA, USA (14.May.2013)

Files

pynusmv-nfm2013.pdf
  • Restricted Access
  • Adobe PDF
  • 197.16 KB
Request a copy
10.pdf
  • Restricted Access
  • Adobe PDF
  • 145.03 KB
Request a copy

Details

Authors
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 performance results showing negligible impact compared to native NuSMV.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

Busard, S., & Pecheur, C. (2013). PyNuSMV: NuSMV as a Python Library. In Guillaume Brat, Neha Rungta, Arnaud Venet (ed.), NASA Formal Methods (pp. 453-458). https://doi.org/10.1007/978-3-642-38088-4_33