Formal specification and simulation of the robot path planner

Simulation software plays a very important role in education and research applications. They provide a safe, easy and flexible environment for developing and testing new methods. However developing a simulation software that reflects the exact behavior of the real system is a difficult and complicated task. In this paper we used hybrid process algebra to build a formal model that describes the exact behavior of the path planner module of autonomous mobile robots. The robot path planner is described by a powerful recursive process. The robot moves in four modes heading-regulation, move-to-goal, move-to-inter-goal, and obstacle-avoidance mode. Each motion mode is described by a process. The overall behavior of the path planner is the result of the communication between the four processes. The developed model is then implemented as simulator for mobile robots.