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.

• Type: Journal
• Year: 2010
• Where: SPIN
• Authors: Marc de Jonge, Theo C. Ruys
• Keywords: Exhaustive Mode, Layered Object-oriented Design, SPIN 2010, SpinJa, Theoretical Computer Science