document.tex

\documentclass[a4paper]{article}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{graphicx}
\usepackage{verbatim}
\usepackage[bookmarks=true]{hyperref}
\usepackage[left=2cm, right=2cm]{geometry}
\usepackage{listings}
\usepackage[dvipsnames]{xcolor}

\definecolor{wow}{RGB}{73,63,72}
\usepackage{stix}
% \usepackage{newtxtext}
% \usepackage{eulervm}

\lstset{morecomment=[l]--,
  commentstyle=\color{NavyBlue},
        basicstyle=\small\ttfamily,
        numbers=left,
        classoffset=0,
        morekeywords={TODO},
        keywordstyle=\color{red}\bfseries,
        classoffset=1,
        morekeywords={class,
                      visible,
                      temporal,
                      TD,
                      TI, 
                      items,
                      modules,
                      connection,
                      predicates,
                      axioms,
                      end,
                      inherits,
                      vars},
        keywordstyle=\bfseries,
        classoffset=2,
        morekeywords={axioms},keywordstyle=\color{green},
        classoffset=0}%



\title{Politecnico di Milano\\
Formal Methods for Concurrent \\
and \\
Real-time Systems\\
Homework project\\
\textbf{Collaborative Robotics Modeling }}
\author{Aldeghi Gabriele \\
  Mantovani Mirko \and
  Sacco Alessio \\
  Sonzogni Stefano}
 \date{\today}
 



% The other logical operators are: \lnot, \land, \lor, \iff
\newcommand{\liff}{\iff}
\DeclareMathOperator{\limply}{\Rightarrow}
\DeclareMathOperator{\future}{Future}
\DeclareMathOperator{\past}{Past}
\DeclareMathOperator{\lastsOp}{Lasts}
\newcommand{\lasts}{\lastsOp_{ee}}
\newcommand{\lastsie}{\lastsOp_{ie}}
\newcommand{\lastsii}{\lastsOp_{ii}}
\newcommand{\lastsei}{\lastsOp_{ei}}
\DeclareMathOperator{\lastedOp}{Lasted}
\newcommand{\lasted}{\lastedOp_{ei}}
\DeclareMathOperator{\always}{Always}
\DeclareMathOperator{\sometimeFuture}{SometimeFut}
\DeclareMathOperator{\sometimePast}{SometimePast}
\DeclareMathOperator{\withinOp}{Within}
\newcommand{\within}{\withinOp_{ee}}
\DeclareMathOperator{\uptonow}{UpToNow}
\DeclareMathOperator{\becomes}{Becomes}
\DeclareMathOperator{\nexttime}{NextTime}
\DeclareMathOperator{\lasttime}{LastTime}
\DeclareMathOperator{\until}{Until}
\DeclareMathOperator{\since}{Since}


\begin{document}
\maketitle
\begin{center}
    \includegraphics[width=7cm]{images/polimi-logo}
\end{center}
\clearpage
{\hypersetup{hidelinks}\tableofcontents}
\clearpage

\section{Formalization of the problem}
\subsection{Problem description}
The TRIO+ model presented in this document aims to formalize the interaction between an operator and a KUKA robot.

The goal of the robot is to move unfinished pieces from the bin area to the tombstone. After the piece has been worked, the robot will move it to the conveyor belt.
The operator is assigned to a supervision role and he will interact physically with the end effector of the machine. The model has to guarantee the safety of the operator as well as the utility constraints.

\subsection{Definitions and Acronyms of Components}
\begin{itemize}
    \item \textbf{R}: The whole KUKA mobile robot
    \item \textbf{EE}:\@ The End-Effector of the robot's arm
    \item \textbf{O}:\@ The Operator that works in the same environment of the Robot and interacts with it
    \item \textbf{L}:\@ The entire Layout in which Robot and Operator work
    \item \textbf{BA}:\@ The Bin Area (top-right)
    \item \textbf{WP}:\@ The single WorkPiece which is transported by the robot
    \item \textbf{HDI}:\@ The Human Device Interface used by the Operator to control the Robot
\end{itemize}

\subsection{Constants}
\begin{itemize}
    \item \textbf{N}:\@ The capacity of the local bin of the Robot
\end{itemize}
\subsection{World discretization}

\subsubsection{Human body parts}
\begin{itemize}
    \item \textbf{Head area}:\@ Highly sensitive areas
    \item \textbf{Arms area}:\@ Very delicate areas
    \item \textbf{Body area}:\@ Delicate areas
\end{itemize}

\subsubsection{Robot parts}
\begin{itemize}
    \item \textbf{Arm}:\@ Consisting of 2 segments and 3 links, the last of which connects the farther segment to the EE
    \item \textbf{End Effector}:\@ The robotic hand of R, capable of holding a WP and releasing it.
    \item \textbf{Cart}:\@ The cart is the main part of the robot, it is what can move across areas in the layout.
    \item \textbf{Local Bin}:\@ The local bin of R is located on top of the cart and is able to contain WPs.
\end{itemize}

\subsubsection{Robot speed}
\begin{itemize}
    \item \textbf{None}:\@ Null speed, the robot cannot move
    \item \textbf{Low}:\@ Low speed, the robot can move every other time instant, which means it will move to an adjacent area at most every 2 time instants
    \item \textbf{Normal}:\@ Normal speed, the robot can move to an adjacent area at each time instant.
\end{itemize}

% \subsubsection{Layout areas}
% We discretized the layout in such a way that the most important and critical areas, in which Human-Robot interaction are very likely to happen, have a fine-grained grid, whereas the other areas, in which the Operator should not be present to assist the Robot, are modeled as bigger blocks in order not to introduce unnecessary complexity in the model and to avoid state space explosion.
% \begin{figure}[htp] 
% \includegraphics[width=\textwidth]{images/layout} 
% \caption{Subdivision of the layout, highlighted areas are the most dangerous ones} 
% \label{fig:layout} 
% \end{figure}

% \clearpage
% The most critical areas are the ones with indices from 1 to 12, particular attention must be paid to L\textsubscript0 too, since it is where the EE and O could be working together. 

% \begin{figure}[htp] 
% \includegraphics[width=\textwidth]{images/layoutnames} 
% \caption{Names of the splitted layout and various areas} 
% \label{fig:layout2} 
% \end{figure}


\subsubsection{Layout areas}
We discretized the layout in such a way that the most important and critical areas, in which Human-Robot interaction are very likely to happen, have a fine-grained grid, whereas the other areas, in which the Operator should not be present to assist the Robot, are modeled as bigger blocks in order not to introduce unnecessary complexity in the model and to avoid state space explosion.

The most critical areas are the ones with indices from 1 to 12, particular attention must be paid to L\textsubscript0 too, since it is where the EE and O could be working together. 

\begin{figure}[htp] 
\includegraphics[width=0.9\textwidth]{images/layoutnames} 
\caption{Subdivision of the layout. The highligthed areas are the dangerous ones.} 
\label{fig:layout2} 
\end{figure}

\pagebreak
\subsection{Assumptions and modeling}
\paragraph{Robot}
The robot is discretized in two parts, the cart and the arm. The cart is such that it can only occupy one area at the time: this is a strong assumption, however it is vital because it reduces the complexity of our model. The arm is modeled by considering two joints and the end effector. The first joint is assumed to be the connection between the cart and the arm, therefore its position is at all times the same as the cart position. The second joint allows broader movement to the arm and it links the first joint to the end effector. The whole arm can reach at most a distance of two adjacent areas. The response of the actuators to a change in the control variables is assumed to be short enough to be modeled as instantaneous.

\paragraph{Human}
The human is discretized in body, head and arms. Each one of the parts can only occupy one area. The movement can only be observed, but not controlled, by the robot.

\paragraph{Bin Area}
We operated under the assumption that the Bin Area is always full, or better, it is never empty in any subarea of its space. With this assumption the KUKA robot will only have to stretch out from an adjacent area and pick as many WP as it wants without having to move to another adjacent area because there are no WP left where it is. 

\paragraph{Local Bin}
The local bin of R is where it stores the WPs in order to transport them from one place to the other. For the sake of simplicity we made as an assumption that the local bin can contain at most 3 pieces, so we could write formulae in a simple way, of course this can be generalized to N pieces in a trivial way.

\subsection{KUKA workflow}
The workflow of KUKA can be described by a FSA, we divided the tasks that R has to perform in 9 main elementary actions, whose formalization can be found in the \textbf{RobotController} TRIO+ class.
Those atomic actions whose name is self-explaining are:

\begin{enumerate}
    \item \textbf{PickFromBinArea}\@ 
    \item \textbf{DropToLocalBin}\@
    \item \textbf{GoToTombstone}\@ 
    \item \textbf{PickFromLocalBin}\@ 
    \item \textbf{DropToTombstone}\@ 
    \item \textbf{PickFromTombstone}\@ 
    \item \textbf{GoToConveyorBelt}\@ 
    \item \textbf{DropToConveyorBelt}\@ 
    \item \textbf{GoToBinArea}\@ 
\end{enumerate}
\clearpage
\subsection{Petri Net of KUKA workflow}
The following Petri net that represents the correct flow of actions that the robot has to perform.
\begin{center}
    \includegraphics[width=18cm]{images/petriNetKuka}
\end{center}

\clearpage
\section{Archi-TRIO model}

\subsection{Class overview}
We organized the model in 12 TRIO+ classes, here we provide an overview of each one and a UML-like diagram to better visualize the connections among them.

\subsubsection{Grid}
The layout is discretized in this class, here we defined the adjacency predicate and the enumeration of subareas of L, as well as other specific predicates for special areas contained in L.

\subsubsection{Sensors}
The main superclass of sensors is \textbf{PositionSensor}, it uses as module the \textbf{Grid} and has 2 predicates: Position(layout area) and moved(), the subclasses which inherits them are the following ones:

\begin{itemize}
    \item \textbf{OperatorHeadPositionSensor}:\@ The sensor for the head of O
    \item \textbf{OperatorBodyPositionSensor}:\@ The sensor for the body of O
    \item \textbf{OperatorArmPositionSensor}:\@ The sensor for the arm of O
    \item \textbf{RobotArmPositionSensor}:\@
The sensor for the arm of O, in which the linkings and constraints are made consistent
    \item \textbf{RobotCartPositionSensor}:\@ The sensor for the Cart position in the layout
\end{itemize}

Then 2 main wrappers are created around the sensors, in which constraints among the various specific sensors are defined:
\begin{itemize}
    \item \textbf{OperatorPositionSensor}:\@ The wrapper sensor for O which imports as modules OperatorHeadPositionSensor, OperatorBodyPositionSensor, OperatorArmPositionSensor and the Grid
    \item \textbf{RobotPositionSensor}:\@ The wrapper sensor for R which imports as modules RobotArmPositionSensor, RobotCartPositionSensor and the Grid

\end{itemize}

\subsubsection{RobotStatus}
In this class we have the main predicates about the state of the robot and of its local bin (isFull, isEmpty), here we also define the targetCartSpeed and targetEESpeed which are the control variables, and currentCartSpeed, currentEESpeed which are read from sensors and defined as a part of the state of the robot itself.

\subsubsection{RobotController}
This is one of the most important classes, it handles all the actions performed by R, it specifies preconditions, axioms with constraints on what should be true while an action is being performed, and the actual sequence of events that the action is composed by.

\subsubsection{SafetyChecker}
Here we define all the constraints necessary for the safety of O in the presence of a working KUKA R around the layout, all the actions performed by R that could cause harm to O are avoided or limited as much as possible.

\subsection{UML diagram}
This diagram shows the connections and hierarchies among classes.
\begin{center}
    \includegraphics[width=16.5cm]{images/ArchiTRIO}
\end{center}
\clearpage
\section{TRIO+ specification}

\subsection{Definition of Grid class}
\input{latexClasses/latexGrid}

\pagebreak
\subsection{Definition of the PositionSensor class}
\input{latexClasses/latexPositionSensor}

\pagebreak
\subsection{Definition of the operator's sensor classes}
\input{latexClasses/latexOperatorArmPositionSensor}
\input{latexClasses/latexOperatorBodyPositionSensor}
\pagebreak
\input{latexClasses/latexOperatorHeadPositionSensor}
\input{latexClasses/latexOperatorPositionSensor}

\pagebreak
\subsection{Definition of the robot's sensor classes}
\input{latexClasses/latexRobotArmPositionSensor}
\input{latexClasses/latexRobotCartPositionSensor}
\pagebreak
\input{latexClasses/latexRobotPositionSensor}

\pagebreak
\subsection{Definition of the state of the robot}
\input{latexClasses/latexRobotStatus}

\pagebreak
\subsection{Definition of the RobotController class}
\input{latexClasses/latexRobotController}

\pagebreak
\subsection{Definition of the SafetyChecker class}
\input{latexClasses/latexSafetyChecker}

\pagebreak
\subsection{Safety Properties}
\input{latex/safety-properties}


% %\subsection{Definition of the robot position sensors}
% \section{Demonstration of Saftety Properties}
% \input{latex/safetyRules}


\pagebreak
\appendix
\section{Area modeling}

Here we provide a sample of the formula that states for every possible combination of 2 cells in the layout, which one are adjacent to each other and which one are not.

\begin{align*}
&\neg Adj(L0, L0) \land Adj(L0, L1) \land Adj(L0, L2) \land Adj(L0, L3) \land Adj(L0, L4) \land \neg Adj(L0, L5) \land \neg Adj(L0, L6) \\
&\land \neg Adj(L0, L7) \land \neg Adj(L0, L8) \land \neg Adj(L0, L9) \land \neg Adj(L0, L10) \land \neg Adj(L0, L11) \land \neg Adj(L0, L12) \\
&\land \neg Adj(L0, L13) \land \neg Adj(L0, L14) \land \neg Adj(L0, L15) \land \neg Adj(L0, L16) \land \neg Adj(L0, L17) \land \neg Adj(L0, L18) \\
&\land \neg Adj(L0, L19) \land \neg Adj(L0, L20) \land \neg Adj(L0, L21) \land \neg Adj(L0, L22) \land \neg Adj(L0, L23) \land \neg Adj(L0, L24) \\
&\land \neg Adj(L0, L25) \land \neg Adj(L0, L26) \land \neg Adj(L0, L27) \land \neg Adj(L0, L28) \land Adj(L1, L0) \land \neg Adj(L1, L1) \land Adj(L1, L2) \\
&\land \neg Adj(L1, L3) \land \neg Adj(L1, L4) \land Adj(L1, L5) \land Adj(L1, L6) \land \neg Adj(L1, L7) \land \neg Adj(L1, L8) \land \neg Adj(L1, L9) \\
&\land \neg Adj(L1, L10) \land \neg Adj(L1, L11) \land \neg Adj(L1, L12) \land \neg Adj(L1, L13) \land \neg Adj(L1, L14) \land \neg Adj(L1, L15) \\
&\land \neg Adj(L1, L16) \land \neg Adj(L1, L17) \land \neg Adj(L1, L18) \land \neg Adj(L1, L19) \land \neg Adj(L1, L20) \land \neg Adj(L1, L21) \\
&\land \neg Adj(L1, L22) \land \neg Adj(L1, L23) \land \neg Adj(L1, L24) \land \neg Adj(L1, L25) \land \neg Adj(L1, L26) \land \neg Adj(L1, L27) \\
&\land \neg Adj(L1, L28) \land Adj(L2, L0) \land Adj(L2, L1) \land \neg Adj(L2, L2) \land Adj(L2, L3) \land \neg Adj(L2, L4) \land Adj(L2, L5) \\
&\land Adj(L2, L6) \land Adj(L2, L7) \land \neg Adj(L2, L8) \land \neg Adj(L2, L9) \land \neg Adj(L2, L10) \land \neg Adj(L2, L11) \\
&\land \neg Adj(L2, L12) \land \neg Adj(L2, L13) \land \neg Adj(L2, L14) \land \neg Adj(L2, L15) \land \neg Adj(L2, L16) \land \neg Adj(L2, L17) \\
&\land \neg Adj(L2, L18) \land \neg Adj(L2, L19) \land \neg Adj(L2, L20) \land \neg Adj(L2, L21) \land \neg Adj(L2, L22) \land \neg Adj(L2, L23) \\
&\land \neg Adj(L2, L24) \land \neg Adj(L2, L25) \land \neg Adj(L2, L26) \land \neg Adj(L2, L27) \land \neg Adj(L2, L28) \land Adj(L3, L0) \\
&\land \neg Adj(L3, L1) \land Adj(L3, L2) \land \neg Adj(L3, L3) \land Adj(L3, L4) \land \neg Adj(L3, L5) \land Adj(L3, L6) \\
&\ldots 
\end{align*}
\end{document}