Treffer: FORMAL SPECIFICATION AND REFINEMENT OF THE NAVIGATION TASKS OF AUTONOMOUS ROBOTS

Autonomous robots are hybrid systems whose role in our daily life is becoming increasingly critical. They are tasked with various activities requiring reliability, safety, and correctness of their software-controlled behavior. Formal methods have been proved effective in addressing development issues associated with these software qualities. However, even though autonomous robot navigation is a primordial function, there is no research dealing with enhancing reliability of the navigation algorithms. Thus, our focus is to investigate this type of algorithms, and specifically path planning, a fundamental and critical functionality supporting autonomy. We formally address the issue of enhancing reliability of the widely-used A* path planning algorithm. In our stepwise 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. In the next step, we use the Z specification language to effect the transformation from the mathematical description into Z schemas. The resulting specification is completely formal. Subsequently, we use the formal theory of refinement in Z 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 effectiveness of our software development approach.