This paper describes an approach to checking OCL expressions of a UML-based system model using CPN state space tools. The OCL is the part of the UML standard used to specify invariant conditions that must always hold for a system model. An approach to transforming a UML-based system model into a CPN model is taken as basis. Some CPN state space functions traverse all nodes of a state space and can be used to demonstrate that a condition holds. In particular, when a UML-based system model is transformed into a CPN model, CPN traversing functions can be used to demonstrate that an OCL expression holds. OCL expressions are transformed into CPN state space functions. These functions list all nodes in which the OCL expression does not hold. Using this information, software engineers can verify the UML-based system model and detect the presence of defects causing the OCL expression violation. Function results depend on the CPN model initial marking. Two OCL expression examples are presented to show how transformation and checking are done.