U2BCerT — Certified UML-to-B Transpilation

U2BCerT is a grammar-to-grammar transpiler from UML state-transition diagrams (defined in PlantUML) to B machines.
The transpiler is specified in the B method and entirely proved using Atelier B.

The approach relies on a clear architectural separation between:

• a utility machine, which encapsulates low-level mutations of the target B machine
• a transpiler machine, which defines the semantic mapping from UML to B

Overview

The screenshot below illustrates the complete toolchain in action:

• the UML state-transition model
• the generated B machine
• the execution and state exploration
• the preservation of invariants during animation

B Specifications

• transpiler.mch
• u2bcert.mch
• u2bcertutils.mch
• Timer.mch
• Controller.mch

Proof statistics

The following figures report the proof statistics automatically generated by Atelier B for the different components of the framework.

Transpiler component

Global U2Bcert machine (monolithic version)

Utility machine