System Modeling Using Event-B: An Insight

There exist several modeling languages and frameworks for formal representation and analysis of systems. This paper aims to present an in-depth survey on Event-B based model checking. Event B is an evolution from the earlier B language. It has drawn reasonable attention both for industrial and academic communities due to its openness towards the iterative refinements which validate designs starting from a high-level abstraction of the system. The Rodin is a tool that provides an open-source implementation platform for Event-B based model checking and mathematical proofs. Researchers across the globe are using Event B for industry automation, design of embedded and safety-critical systems, and in many more areas. The manuscript presented a well-researched classification considering diverse broad fields where Event-B modeling is applied. Accordingly, research gaps have been identified to highlight future research directions and application domains for event B.