 Earlier tools provided a front-end to work with Rebeca code, and to translate the Rebeca code into input languages of well-known and mature model checkers (like SPIN and NuSMV) and thus, were able to verify their properties.Rebeca, since 2005, is supported by a direct model checker based on Modere (the Model checking Engine of Rebeca).Modular verification and abstraction techniques are used to reduce the state space and make it possible to verify complicated reactive systems.