In this paper, we present a method and a tool to build symbolic labelled
transition systems from B specifications. The tool, called GeneSyst, can take
into account refinement levels and can visualize the decomposition of abstract
states in concrete hierarchical states. The resulting symbolic transition
system represents all the behaviors of the initial B event system. So, it can
be used to reason about them. We illustrate the use of GeneSyst to check
security properties on a model of electronic purse.