Computation of Hierarchical Transition Systems to Document Refined Event-B Models
Nicolas Stouls · 2008
Abstract—To document a formal model and to explain it to non specialists in formal methods, the usual approach is to use another formalism which does not require any expert skill and which gives a second viewpoint of the same model. According to this approach, we proposed in a previous paper to build a symbolic labelled transition system (SLTS) to describe behaviours of a B model. Extending this work, we now introduce hierarchies in SLTS in order to take into account the refinement process and to exhibit links between description levels. In this paper, we propose a formal definition of hierarchical-SLTS (HSLTS) and we extend the SLTS generation method in order to build a HSLTS which represents behaviours of an event-B refined model.