Formal Verification and Implementation of Obstacle Avoidance on NAO Robot

Project Title

Formal Verification and Implementation of Obstacle Avoidance on NAO Robot

Project Area of Specialization RoboticsProject Summary

In the growing age of automation and robotics, navigation of autonomous robots is of utmost importance. To move from its present location to a preset destination is a prime objective of any mobile autonomous robot. The inability to avoid obstacles in its path can render it useless. Without this ability the robot will be fragile, will have limited use, and may prove to be dangerous to humans, the environment, or itself. Thus, the ability of a robot to avoid obstacles while traversing from one place to another has been the subject of many research projects in the field of Mechatronics Engineering. Many algorithms exist for the implementation of path planning such as Potential Field Histogram, Bug Algorithm, Edge Detection, each with its own pros and cons.

Failures of software due to small glitches or unforeseen errors has been concerning engineers and programmers everywhere. Formal verification is a tool that verifies and validates the correct working of a software with respect to some formal property using formal methods of mathematics. In order to formally verify a system, it must be converted into a simpler verifiable state. The system in specified as a set of states with transitions in between them, called a Finite State Machine (FSM). The two most popular methods of formal verification are language containment and model checking. Model checking consists of traversing the FSM and verifying if the system satisfies a particular property.

Many robot simulating tools are present such as, MATLAB or Workspace. Robot Operating System (ROS) is a tool that provides services for a system with heterogenous clusters. It is multilingual and contains packages for many robots common in industry, thus giving its users the ability to simulate them. A ROS project typically consists of nodes, where each node deals with a specific task. The nodes communicate with each other through topics. Messages are sent to these topics by nodes, where other nodes may subscribe to a topic to obtain the message present on it.

In this research, a biped robot is used to avoid static obstacles in a dynamic environment. It is first simulated using Robot Operating System (ROS) where an environment in constructed using Gazebo package. The obstacles in the environment will be placed in different positions for each run, but they will remain stationary. Our algorithm is thenphysically implemented on the NAO v6 robot. The environment in ROS is depicted based on the real environment. Formal verification of the algorithm is performed using UPPAAL, a model checking tool.

Project Objectives

The objective of our project is to implement and formally verify a path planning algorithm. We intend to first simulate our algorithm on NAO robot using V-REP (Virtual Robot Experimentation Platform) and then physically implement it on NAO v6 as well. We will then formally verify our algorithm using UPPAAL, a model checking tool. 

Project Implementation Method

The objective of our project is to implement and formally verify a path planning algorithm. We intend to first simulate our algorithm on NAO robot using V-REP (Virtual Robot Experimentation Platform) and then physically implement it on NAO v6 as well. We will then formally verify our algorithm using UPPAAL, a model checking tool. 

Benefits of the Project

Automation and robotics has taken the engineering world by storm. The demand for mobile robots that work without any human intervention is increasing day by day. Whether it’s a cleaning robot, or an industrial robot to move materials, path planning is the foremost objective to develop mobility. Many mobile robots only have the ability to traverse in familiar, constrained environments. Advancements in robotics led to robots that can localize themselves and navigate through an unfamiliar environment. Robots that can create maps of an unknown environment and even travel in rough terrains have also been developed. For a robot to move from one point to another in a real environment, it will encounter all kinds of obstacles. The first rule in robotics, is to do no harm to humans, the environment, and itself. A mobile robot if not programmed correctly can prove fatal to human life. Thus, the ability of that robot to avoid these obstacles during its travel is the pre-requisite of any mobile robot. In order to avoid these obstacles, the robot will have to change its straight-line trajectory. Much research has been done on this subject. There are many algorithms that solve this problem, each with its merits and demerits. 

This project simulates, implements, and formally verifies path planning of a biped humanoid robot NAO. The robot plans its path from its original position to a preset destination as indicated while avoiding obstacles in its path. The scope of this thesis is limited to static obstacles that may have different locations.

Technical Details of Final Deliverable

The final deliverable will be in three parts:

a) Simulation of path planning using NAO model in V-REP, in a static unknown environment. 
b) Physical implementation of the path planning algorithm on NAO robot in a static unknown environment.

c) Formal verification of the algorithm using UPPAAL.

Final Deliverable of the Project HW/SW integrated systemCore Industry EducationOther IndustriesCore Technology RoboticsOther TechnologiesSustainable Development Goals Sustainable Cities and CommunitiesRequired Resources

Item Name	Type	No. of Units	Per Unit Cost (in Rs)	Total (in Rs)
			Total in (Rs)	70000
Lasani Wood	Equipment	30	1000	30000
Manufacturing cost of Arena	Equipment	40	1000	40000