In order to formally analyze the system properties, syntax and semantics based on a transition system are given. The model is composed of interleaving concurrent processes communicated by shared variables. Also, some extensions are incorporated into the operational formalism, such as shared variables communication and synchronous communication between processes. First at all, the size of the model is reduced, and then translated into the model checker input language. The approach is illustrated with a real example in which we verify a global property by means of the composition of properties that have been checked separately for the essential and the implementation model.