Verify your system using
Spin with SpinRCP.

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.