From a Solution Model to a B Model for Verification of Safety Properties

In the context of safety requirement engineering, model transformation is a task of interest. Indeed, it allows us to keep all the requirements while switching from one point of view to another. The presented work assumes that a valid solution has been found and proposes an approach in order to build a valid implementation.As some fine dynamic properties are integrated into the specification, high-level Petri nets are used to specify and verify the solution. Then, considering an industrial railway context, the transformation of the Petri net model in order to provide an input to a B process is considered. This last consideration leads to a proposition of a systematic direct transformation of the Petri net model into abstract B machines. The approach is illustrated by a theoretical railway example. The limitations of this approach are discussed at the end of the paper and some prospects are detailed.