On Model Checking of a Robotic Mechanism

Abstract

Developing robot control systems can get complex even for small number of functions to be carried by the robot. Finite state machines are representing a frequent approach to model complex systems in a formal way. In this paper we are presenting a methodology for modelling the kinematics of a robotic mechanism represented by a sequence of bodies linked by joints. Each movement is decomposed as a sequence of rotations and translations and a finite state machine modelling the behavior of each of these is built.