Abstract:In today’s general trend for ubiquitous computing and software definition, formal methods have gradually become an important way to guide the definition of software requirements, analyze software design schemes, and verify the correctness of software products, which penetrates the entire life cycle of software engineering. Event-B, as a “correct by construction” method, supports the application of formal methods in software engineering. This paper classifies and expounds on the existing formal methods in software engineering based on Event-B, which are mainly divided into Event-B control structure, object-oriented Event-B, reusable Event-B, as well as real-time Event-B models. It also summarizes the support from various Event-B models for the whole life cycle of software development and provides references for the formal methods in software engineering.