Adding SAT-based model checking to the PyNuSMV framework

Details

Supervisors

Pecheur, Charles

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] en sciences informatiques

Abstract

NuSMV is an open-source reimplementation and extension of the well known SMV model checker developed at Carnegie Mellon University. While this tool provides a rich set of high performance, state of the art verification features; the size and complexity of its code base make the extension and customization of this tool uneasy. In order to alleviate that problem, PyNuSMV was developed at Louvain Verification Lab as a simpler platform to implement verification tools for new logics in Python. However, in its current version, PyNuSMV is limited to symbolic model checking with BDDs. This thesis proposes an extension of PyNuSMV which features SAT-BMC capabilities available in NuSMV. After that, it describes two experiments that were made to validate the usefulness and performance of our addition to the framework. The first one consists in an implementation of an LTL bounded model checker in Python while the second implements a diagnosability test tool which shows how SAT-BMC tools working with multiple parallel traces can be developed using our addition to the framework. The performance evaluation made in the scope of both experiments revealed that the verification tools developed using our addition to PyNuSMV only add a low overhead compared to an equivalent verification done with NuSMV and, in some cases significantly outperforms what is feasible with the regular NuSMV.