The objective of the following project is to describe a formal model of the interaction of an Human Operator and a Robot. The Robot to be modelled is analogous to the KUKA KMR-iiwa which is a manipulator and mobile robot, used mainly for industrial use: welding, assembly, loading and unloading.
The scenario is one of Robot Human Collaboration where the Robot has to aid the operator in performing a given task. Specifically the Robot has to bring Work Pieces from a Global Bin to a Work Station.
After being elaborated in some fashion by either additional machinery or the Operator, the pieces are placed on a Conveyor Belt.
Normally the Robot operates in a sort of loop, going back and forth from the Global Bin to the Work Station in order to bring pieces.
It's also possible for the Operator to give the Robot additional commands.
For a more precise description of the Robot tasks it's possible to refer to the graph below.
The robot enviroment is formalized as follows.
The formal description of the system is done using TRIO formal language and can be found here
A simplified version of the model has been verified using Zot model checker
In order to run the script Docker must be installed
./run.sh zot FM.lisp