Author Description

Event-B is a formal method to develop the computer software in modeling level and analysis of dependable applications. It is based on abstract machine notation. It is supported by an open and extendable Eclipse-based tool set called Rodin. In recent years, Event-B and Rodin have been used to model complex real world systems and also prove consistency properties of them. However, refinement that kind of systems which have difficult proofs is not an easy task, so Event-B design pattern just another model used to the formalization of a typical problem.