Model transformation is an interesting task, which could take advantage of several modelling languages, and meanwhile should respect all the safety requirements. The presented work studies the translation from a valid design solution to a valid implementation, which is a mapping method from coloured Petri nets to abstract B machines. Both modelling languages are well known formal methods in the context of safety requirement engineering. The Petri nets are widely accepted by French railway engineers because of a fine graphic representation and their dynamic analysis properties. The B machine offers verified software development based on B language, which has already been applied in some safety-critical systems. The proposed model translation technique will help to bridge the gap between these two formal methods. This paper shows the systematic process of the translation, which is also illustrated by several case studies. The limitations and future efforts are discussed at the end of the paper.

Coloured Petri nets B method, modelling languages translation, critical system