Engineering Verified Model Transformations through a Proof-Based Language Workbench
TL;DR
BCerT is developed, an extension of the Meeduse language workbench originally dedicated to the formal modeling of domain-specific languages, allowing animation and model checking with ProB, as well as theorem proving with Atelier B.
Abstract
Model-driven transformations play a central role in MDE processes, yet their correctness is most often validated through testing or simulation. However, in contexts where critical scenarios may compromise system integrity or certification objectives, stronger guarantees are necessary. This paper investigates how the B method can support transformation engineering through verified formal specifications. To this end, we developed BCerT, an extension of the Meeduse language workbench, originally dedicated to the formal modeling of domain-specific languages. In our approach, transformations are defined as B operations or B events, allowing animation and model checking with ProB, as well as theorem proving with Atelier B. We discuss three complementary specification strategies: (i) a rule-oriented modeling approach optionally controlled with CSP||B; (ii) a property-driven operational B specification in which the transformation is expressed as a relation constrained by invariants; and (iii) an Event-B system capturing the transformation as atomic events focused on the end state. The approach is illustrated through two applications: the verification of a Truth Tables to Binary Decision Diagrams transformation presented at the Transformation Tool Contest, and the development of U2BCerT, a certified transpiler from UML state machines to Event-B.