Generating Hierarchical State Based Representation From Event-B Models

Many properties of a system may not be obvious just by a quick inspection of the corresponding Event-B model. Users typically rely on animation, scenario analysis, and inspection of state transition graphs for discovering certain behavior of the system. We propose a methodology for generating a hierarchical representation of the system for visualising Event-B models. Our representation is succinct and it provides multiple views to aid in better comprehension of the Event-B models.