A set of design oriented scientific tools to assist abstract B machine specification

The B method is known to be efficient, as a process of certifiable software implementation building in the domain of guided transports. There is important work to be performed using the informal specification before entering the B process. The upstream requirement analysis may be assisted with some graphical tools using UML notations. Nevertheless, the main problem to be solved may be the choice of the adequate tool. Currently, there are several kinds of diagrams in the UML notation and they are partially redundant. Considering a more general point of view, a main human contribution is to choose the representation which is specifically adapted to the considered assessment problem.