Verify your system using
Spin with SpinRCP.

SpinRCP - An Integrated Development Environment for the Spin Model Checker.


Brief Description

SpinRCP is an integrated development environment (IDE) for the Spin model checker that is used for verifying the correctness of concurrent and distributed systems. Using SpinRCP, it is easy to enter, edit, examine, and check syntax of the models that represent the systems to be analyzed, to check redundancies in models, to specify the required properties of models, to graphically represent processes and never claims derived from the specified properties in the form of nondeterministic final state machines, to enter or select many various simulation and verification parameters, to perform verification and random, guided, or interactive simulation and to transform a Spin simulation trail to a standard Message Sequence Chart (MSC). SpinRCP is implemented in Java as an Eclipse Rich Client Platform (RCP) product.

Different Perspectives of SpinRCP

Note: All presented screenshots on this web site are obtained from SpinRCP Version 3.1.0 installation under Windows 8.1 Pro. The default white color of window borders is changed to light blue on purpose for better contrast on the bright background.