الفهرس 
chapter 1: IntroductionOnly 14 pages are availabe for public view
 |  | from | 85 |  |  |
| | | from | 85 | | |
Abstract
Computer systems (software and Hardware) share in different fields like mechanical
engineering, civil engineering, medicine, traffic control and aerospace. Actually, these sys-
tems are critical and should have low percentage of error which sometimes tends to zero. So
system verification after design or implementation becomes a necessity. Verification means
-in simple words- investigate if a system model (design or implementation) satisfies system
specifications. Robots are one of the automated systems that used in the previously men-
tioned fields. A robot is a device which has a manipulator arm, a multi-joint multi-fingered
hand, a wheeled or legged vehicle, a free flying platform, or a combination of these. Robot is
usually equipped with actuator and sensors under the control of a computing system. The
robot performs tasks by executing motions in a workspace where it is required from the
robot to decide automatically what motion to execute in order to achieve that task, this is
known as motion planning problem. Through this work the model checking-one of popular
verification method- is used in trajectory planning verification of a Khepera robot. We
put the reader in the context of the model checking method and its advances like symbolic
model checking. An over view of robot motion planning is introduced and mathematical
model of the khepera robot also. Depending on the model of the robot, we added a safety
condition on the robot to protect it from doing useless rotation which may cause motor
(or any hardware part) failure. The military has attempted to insert robotic technology
into aerial platforms since World War I, where attempts primarily focused on remotely
controlling dirigibles. The first real breakthrough was in World War II when a modified
B-17 successfully performed unmanned flights. Unmanned Aerial Vehicles (UAVs) had had
much more success than their ground counterparts because they do not have to contend
with obstacles. Nowadays after the breakthrough of motion planning, Unmanned Grounded
Vehicles can contribute well in the war. A new specification which helps in specifying a