Model checking in object-oriented Petri nets

We present model checking techniques for verifying an object oriented Petri net modeling language (RPOO). Our intention is turn the application of model checking on model-based software development more feasible. In order that we provide means of specifying objects properties regardless Petri nets details. We use Petri nets semantics just to construct the models state space. We present our algorithms to evaluate properties expressed in branching-time temporal logic CTL. We deal with explicit representation of state space emphasizing its OO features. Besides, we remark the results of some applications of our model checker.