The SpinJa model checker

SpinJa is a model checker for promela, implemented in Java. SpinJa is designed to behave similarly to Spin, but to be more easily extendible and reusable. Despite the fact that SpinJa uses a layered object-oriented design and is written in Java, SpinJa's performance is reasonable: benchmark experiments have shown that, in exhaustive mode, SpinJa is about five times slower than the highly optimized Spin. For bitstate verification runs the difference is only a factor of two. © 2010 Springer-Verlag