Proof of Properties of a Syntax Analyzer of Robotic Mission Plans

In order to enhance the dependability of robotic missions designed with the help of the language PILOT, an incremental syntactic analyzer has been built. We have shown, with the help of the SWI-Prolog tool, that the analyzer allows to build all and only all the plans which are syntactically correct under some size. This proof has been done only for plans whose size is less than a threshold, because of a combinatory explosion problem inherent to the working of Prolog and to the used approach. In order to show the validity of the incremental syntactic analyzer for all plans, without any size constraint, we turned to the use of proof-based approaches, and particularly towards PVS tool. This paper deals with the modeling and verification of PILOT plans and their properties with the help of PVS, in order to prove the above properties of the incremental syntactic analyzer of PILOT.