Xtend Transformation from PDDL to Event-B.

PDDL is a de facto standard language for formally describing planning problems. It is equipped with dynamic tools for executing PDDL descriptions. But, it is not equipped with static tools allowing to reason a priori on the correction of the PDDL descriptions. To remedy this shortcoming, we have designed, produced and tested a tool called PDDL2EventB in order to automate the approach and the systematic translation rules from PDDL to Event-B. This allows a formal static verification of PDDL descriptions and exploit the static tools associated with Event-B. To achieve this, we successfully used the Xtext MDE tool creating an integrated development environment specific to the PDDL language, and the Xtend tool to implement our transformation and produce the Event-B models according to a top-down approach.