Coupling event-B/ProB for the analysis of the software architecture evolution described in PDDL

Abstract

The PDDL language is used to formally describe planning problems. It has tools called planners to solve planning problems described in PDDL. Equally, it has plan validation tools to validate the solution plans. Our automatic approach to transform a planning problem written in PDDL to Event-B method allows the use of the correct-by-construction paradigm associated to Event-B formal method. We propose a modeling PDDL for Software Architecture Evolution. Then, we translate our PDDL description in Event-B using our plugin PDDL2EventB. Finally, we reason on the Event-B model generated by the use of ProB including: animation, model checking and deadlock-free.