Formal specification, refinement, and implementation of path planning

Abstract

We investigate navigation algorithms, and specifically path planning, a fundamental function of autonomous robots. We formally address the issue of enhancing reliability of the widely-used A* path planning algorithm. In our step-wise refinement process, we capture successively more concrete specifications by transforming a high-level specification into an equivalent executable program. To elaborate an initial representation of the A* algorithm, we express it in an abstract and intuitive, yet formal, description. We use traditional mathematical concepts, such as sets, functions and predicate logic to capture this description. We then use the Z specification language to effect the transformation from the mathematical description into Z schemas, thus obtaining a formal specification. We use CZT to perform syntax and type checking and the Z/EVES tool to automatically prove some properties about the specification. Subsequently, we use the Z formal refinement theory to generate the implementation specification. This stage involves both data and operation refinement and is carried out in several basic sub-steps. A Java-based simulation prototype that mirrors the implementation specification is developed in order to demonstrate the applicability of our software development approach.