Object-oriented modelling is known to be an appropriate approach for representing concurrent and distributed systems. Besides having an appropriate and efficient way for modelling these systems, one needs a formal verification approach for ensuring their correctness. Therefore, we have developed an actor-based model for describing such systems.

We use temporal logic to specify properties of a model, and various verification methods for verifying that the model meets its specification. The state explosion problem in model checking can be avoided by using techniques that replace a large component by a smaller component which satisfies the same properties. We introduce a notion of simulation between structures, which guarantees that a positive check of universal, stuttering-invariant properties on simulations also hold on the systems they simulate. Simulation can be used in the compositional verification of the whole system.

Also, we have developed a tool for translating Rebeca codes to SMV. Therefore, we now can model check Rebeca codes by SMV model checker.