Automatic planning has a de facto standard language called PDDL for describing planning problems. The dynamic analysis tools associated with this language do not allow sufficient verification and validation of PDDL descriptions. Indeed, these tools, namely planners and validators, allow a posteriori error detection. In this paper, we recommend a formal approach coupling the two languages Event-B and PDDL. Event-B supports a formal development process based on the refinement technique with mathematical proofs. Thus, we propose a refinement strategy for obtaining reliable PDDL descriptions from an ultimate Event-B model that is correct by construction. The correctness is guaranteed via the verification and validation tools supported by Event-B. We have chosen the MICONIC application managing modern elevators to illustrate our approach while recognizing that the MICONIC application is already modeled in PDDL without formal proof of its correctness.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 email@example.com
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 firstname.lastname@example.org