TCS / Personnel / Tuomas Launiainen / PSL Observer

PSL Observer for NuSMV

The PSL Observer is a prototype implementation of the observer-pattern based algorithm of model checking PSL safety properties that is described in my Master's thesis, Model checking PSL safety properties.


The source package is available here: NuSMV-psl-observer.tar.gz. It is distributed under the LGPL 2.1 license. Note that the implementation is a prototype, and should not be used for anything besieds evaluating the algorithm! The program can only handle a single module and PSL specification in its input file.

Compiling and running the benchmarks

Run "make" in the top directory. You'll need gnuplot, the file from in the MiniSat directory, and the file bin.tar.gz from in the top directory.

Latest update: 5 June 2009.