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.

Source

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 minisat2-070721.zip from http://minisat.se/MiniSat.html in the MiniSat directory, and the file bin.tar.gz from http://es.fbk.eu/people/tonetta/tests/tcad07/ in the top directory.


Latest update: 5 June 2009.