This paper presents new principles of solving a model synchronization problem based on the definition of synchronization mechanisms in terms ofprocess calculus and a description of their correctness properties in terms of temporal modal logic with further verification by applying rules of logical inference. The main correctness properties of model synchronization process and basic features of designing model synchronization tools are discussed.