Problems and Objectives. In Human-Robot Collaborative (HRC) applications, operators and robots work in a common space. Their close interactions increase the likelihood of direct physical contacts either due to the intrinsics of the operations (e.g., tools, motions, etc) or behavior of the operator (e.g., mistakes, misuses, instruction misunderstanding, etc). Unintended physical contacts may lead to hazardous situations for the operator. In order to identify and avoid such situations as far as possible, we need to define and develop a comprehensive approach for safety assessment of HRC applications, that includes: - Complying standards of risk analysis [10] and robotic safety [9]. - Ensuring the absence of unforeseen hazardous situations during design of systems by formal verification. - Focusing on hazards caused by behavior of operators. - Identifying hazards automatically, hence none is unconsidered, however keeping a human-in-the-loop attitude to interact with safety analyzers in order to use their operational perspective and experience. - Estimating the gravity of identified hazard as a quantified value-named risk, which is computed on the basis of detailed analysis of the whole system (e.g., the severity of the injury that it causes). - Suggesting proper treatments known as Risk Reduction Measures (RRM), which decrease the risk down to a negligible threshold.
Our approach to provide the above mentioned factors exploits formal methods
for the specification and verification of system properties and is centered on the
following steps: (i) Observe a real HRC case study to achieve a common
understanding with robotic community about safety requirements, hazards and their
relevant treatments, (ii) Define a coherent methodology to describe applications
and verify if they provide a minimum level of safety, (iii) Build a modular model
of the case study by use of a decidable fragment of the TRIO metric temporal
logic [
Literature Review. We performed an extensive literature search on current
safety analysis research in robotics, and found that none of them recognizes the
operator as a proactive factor. There is no focus on the safety violations that
are caused by human activities and interactions with robots. Also there is no
compatibility with international standards [
Two main approaches to determine the behavior of human operators in
literature are: cognitive and task-analytic models [
Task-analytic approaches, instead, model all the possible combinations of
hazardous situations, regardless of their cognitive reasons, by hierarchical
structures of tasks to be then decomposed into smaller functional units (atomic
actions). Execution and sequence of actions are usually controlled through pre- and
post-conditions. Examples of such approaches include the User Action Notation
in [
In addition, traditional formal approaches such as FMEA (Failure Mode and
Effects Analysis) and FTA (Fault Tree Analysis) are not well-suited for HRC
applications because they do not capture hazards due to human factors or
combinations of hazards. They also produce a large amount of repeated information
and false positives and are dependent on the analyzers team which makes them
less generic [
Other examples of combining formal and informal solutions are [
Input by the Safety Engineer
O L
T
R
Hazards Module Risk Estimation
Module RRMs Module risk >T
Zot Update or Modify according to safety Eng. suggestions List of interrupted actions and hazards.
In order to make it easier for safety engineers to build formal models, we introduced a general model, depicted in Fig. 1, which can be tailored to different scenarios with a minimum amount of required input. It consists of four main modules written in TRIO. The ORL-module includes formal descriptions for operator O, robot R and layout L. The descriptions of O and R are generic descriptions and there can be multiple instances of each of them, according to the case study (e.g., defining predicates that describe parts of body and robot). The rule set related to L divides the layout into fine-grained regions so that positioning of O and R and their movements are expressible.
The model also includes a set of rules T concerning the definition of tasks, what O and R are supposed to execute in L. The definition of tasks varies for different applications,thus the safety analyzer provide them as input. Tasks are broken down into a set of elementary actions that are the smallest possible functional units and are executed either by the operator or the robot. Each action is defined by its pre and post-conditions and can be in one of the following states at any given time: “not started” (ns), “waiting” (wt), “executing” (sfex), “executing together with at least one RRM ” (exe), “hold” (hd), “exit” (exit), and “done” (dn). The wt phase is defined only for operator actions that asserts preC of the action are true but opFig. 2: In addition to their guards, black erator hesitates to start the execuand blue edges also have 9i(riski T ), tion.The total state of the model is the while red ones have 9i(riski > T ). Cartesian product of the state of actions and the value of predicates (e.g., positions, risk values).
Figure.2 displays a state diagram representing the behavior of actions and shows how their state changes.
The Hazards module includes formal definition of situations generating a
significant hazard. It contains a set of formulae that use modal operators such as
Contact;( ; !) Approach;( ; !) Depart;( ; !) , where ; ! are parts of R and
O, to express the hazardous situations. Consequences of different hazards and
measuring their severity are explained exhaustively in [
The Risk Estimation module includes the information regarding the
computation of risk of hazards according to the hybrid method reported in [
Finally, the RRM module defines all the RRMs that should additionally be present in the model when a hazard occurs in a trace of the model. At Each verification iteration, we check the full formal model explained above, against the property Alw(8x(riskx T )). The property actually asserts that for all the occurred hazards x, the value of risk should always be less than en acceptable threshold T . The Zot explores the state-space of the model and looks for states that conform with at least one hazard definition. If such state is detected and its risk value is non-negligible, then verification is failed and Zot outputs the problematic state so that we can refine the model.
Case Study. We studied an assembly task in which workpieces should be machined into fixtures attached to a pallet. A small collaborative robot, Kuka lightweight manipulator, carrying an interchangeable screwdriver/gripper endeffector is installed on a cart in close position to both the pallet and the operator. The work-cell is equipped with cameras and sensors that detect the position of robot and operator. The work-cell of the scenario and its division is shown in Figure. 3(a).
In the task, one of the executors (operator/robot) is supposed to set a workpiece (wp) in place from a bin into the tombstone fixtures and holds the wp until the other executor (robot/operator) completes the screwdriving. The operator chooses the executor of each part of the task and sends relevant commands to the robot through an interface.
The user-provided description of the task is broken into several actions, each formalized through a set of pre-/post-conditions. This is done through an intermediate stage of translating the textual description to UML notation, in particular activity diagrams (see Figure.3(b))1.
We found out about some hazardous situations that have been overlooked in earlier versions of the model, through the verification process. For example different timing behavior of the operator and robot (considering the timeout of the operator actions) can lead to different circumstances. Also replacing actions of a task with actions from elsewhere (e.g., with actions of different tasks, that may happen due to misunderstanding of the task instructions) by the operator creates situations that have not been anticipated initially. 1 The complete formal model and the experiments can be found at repository. (a) (b)
Further Work. SAFER-HRC takes into account also the concurrency of multiple actions, in particular actions that must be executed by the operator and by the robot in full coordination. It explores all the different order of execution of actions. For example, traces ai; aj and aj ; ai achieve the same goal, but executing ai after aj causes a hazard that does not exist in the first trace (e.g., , a change in positioning of the operator w.r.t the robot). In the remaining year of my phD, we plan to exploit this feature of the work using larger scale and more complex case studies. Next we will develop a stand alone framework for interactive risk assessment of HRC applications for system designer and safety engineers. In a longer-term perspective, we aim to empower the framework with libraries that define most of the tasks that a robot performs (e.g., Kuka lightweight manipulator). Therefore, we believe our framework will suit for real HRC scenarios.