Abstract
Refinement process applied to UML2.0 Sequence Diagrams (SD) is adopted to deal with the complexity of modeling distributed systems. The various steps leading to the checking of the refinement of SDs theoretically as well as practically are explained. A refinement relation possessing the necessary properties, is formalized; its implementation in the Event-B method is proposed in order to check the correctness of the refinement of SDs, and to verify some safety, liveness properties and the termination of the new introduced events.