BCerT | BCerT

BCerT is an Eclipse-based MDE tool dedicated to the formal specification, verification, and execution of model-to-model transformations and grammar-to-grammar transpilers using the B method. It supports transformations for Ecore metamodels and Xtext grammars.

Note: The public version of BCerT currently supports Classical B as well as the B System dialect of Event-B used in Atelier B. The integration of the Rodin format of Event-B is under experimentation and will be available in a future release.

Papers

Akram Idani, German Vega. Engineering Verified Model Transformations through a Proof-Based Language Workbench. ACM SIGPLAN International Conference on Software Language Engineering (SLE’2026). Accepted long paper.
Akram Idani, Transpilation Meets the B Method. Festschrift in Honor of Jean-Raymond Abrial, edited by Egon Börger and Yamine Aït Ameur. Accepted book chapter.

Features

Execution: Formal B specifications of the transformation can be executed on concrete models, producing target models while preserving invariant properties.
Step-by-step debugging: BCerT integrates with Meeduse debugging facilities, allowing developers to execute transformations step by step and inspect intermediate states.
Trace replay: Replays (backward and foreward) execution traces so that transformation logic can be understood.
Batch transformation runner: Transformations can be executed on multiple models at once using sequential execution or parallel execution for improved performance on large model collections.

👉 Installation guide

License

BCerT is distributed under the Eclipse Public License v2.0 (EPL-2.0).

Eclipse Public License — v 2.0

THE ACCOMPANYING PROGRAM IS PROVIDED UNDER THE TERMS OF THIS ECLIPSE PUBLIC LICENSE ("AGREEMENT"). ANY USE, REPRODUCTION OR DISTRIBUTION OF THE PROGRAM CONSTITUTES RECIPIENT'S ACCEPTANCE OF THIS AGREEMENT.
View the full license text