Abstract
The UML language is used to describe the structure and behavior of software visually. Timing diagrams in UML can be used to define the behavior of different objects over a time range and give their states and interactions. However, UML is prone to ambiguity, lacks accurate semantics, and is difficult to analyze and verify dynamically through tools. The formal method can solve the shortcomings of UML semantically. This paper uses Event-B as the formal specification method of the UML model diagram, mainly for the timing diagram of UML, and gives its conversion method to Event-B. Finally, an elevator example is combined to illustrate the conversion method and process of the UML model diagram to a formal specification.