SAFER-HRC: Safety Analysis Through Formal vERification in Human-Robot Collaboration

  • Mehrnoosh AskarpourEmail author
  • Dino Mandrioli
  • Matteo Rossi
  • Federico Vicentini
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9922)


Whereas in classic robotic applications there is a clear segregation between robots and operators, novel robotic and cyber-physical systems have evolved in size and functionality to include the collaboration with human operators within common workspaces. This new application field, often referred to as Human-Robot Collaboration (HRC), raises new challenges to guarantee system safety, due to the presence of operators. We present an innovative methodology, called SAFER-HRC, centered around our logic language TRIO and the companion bounded satisfiability checker Zot, to assess the safety risks in an HRC application. The methodology starts from a generic modular model and customizes it for the target system; it then analyses hazards according to known standards, to study the safety of the collaborative environment.


Safety analysis Formal verification Safety rules Human-robot collaboration 


  1. 1.
    The Zot bounded satisfiability checker.
  2. 2.
    Baracchi, L., Cimatti, A., Garcia, G., Mazzini, S., Puri, S., Tonetta, S.: Requirements refinement and component reuse: the FoReVer contract-based approach. In: Handbook of Research on Embedded Systems Design (2014)Google Scholar
  3. 3.
    Baresi, L., Kallehbasti, M.M.P., Rossi, M.: How bit-vector logic can help improve the verification of LTL specifications over infinite domains. In: Proceedings of SAC, pp. 1666–1673 (2016)Google Scholar
  4. 4.
    Dhillon, B.S., Fashandi, A.R.M.: Safety and reliability assessment techniques in robotics. Robotica 15(6), 701–708 (1997)CrossRefGoogle Scholar
  5. 5.
    Espiau, B., Kapellos, K., Jourdan, M.: Formal verification in robotics: why and how? In: Giralt, G., Hirzinger, G. (eds.) Robotics Research, pp. 225–236. Springer, London (1996)Google Scholar
  6. 6.
    Fung, P., Norgate, G., Dilts, T., Jones, A., Ravindran, R.: Human-in-the-loop machine control loop. Patent nr. US 5116180 A (1992)Google Scholar
  7. 7.
    Furia, C.A., Mandrioli, D., Morzenti, A., Rossi, M.: Modeling Time in Computing. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2012)zbMATHGoogle Scholar
  8. 8.
    Guiochet, J.: Hazard analysis of human-robot interactions with HAZOP-UML. Saf. Sci. 84, 225–237 (2016)CrossRefGoogle Scholar
  9. 9.
    Guiochet, J., Do Hoang, Q.A., Kaaniche, M., Powell, D.: Model-based safety analysis of human-robot interactions: the MIRAS walking assistance robot. In: Proceedings of the International Conference on Rehabilitation Robotics (ICORR), pp. 1–7 (2013)Google Scholar
  10. 10.
    International Electrotechnical Commission: IEC 61882, Hazard and operability studies (HAZOP studies) Application guide (2001)Google Scholar
  11. 11.
    International Standard Organisation: ISO10218-2:2011, Robots and robotic devices - Safety requirements for industrial robots - Part 2: Robot Systems and IntegrationGoogle Scholar
  12. 12.
    International Standard Organisation: ISO12100:2010, Safety of machinery - General principles for design - Risk assessment and risk reductionGoogle Scholar
  13. 13.
    International Standard Organisation: ISO13849-1:2015, Safety of machinery - Safety-related parts of control systems - Part 1: General principles for designGoogle Scholar
  14. 14.
    International Standard Organisation: ISO14121-2:2007, Safety of machinery - Risk assessment - Part 2Google Scholar
  15. 15.
    International Standard Organisation: ISO/TS15066:2015, Robots and robotic devices - Collaborative robotsGoogle Scholar
  16. 16.
    Leveson, N.: Engineering a Safer World: Systems Thinking Applied to Safety. MIT Press, Cambridge (2011)Google Scholar
  17. 17.
    Machin, M., Dufossé, F., Blanquart, J.-P., Guiochet, J., Powell, D., Waeselynck, H.: Specifying safety monitors for autonomous systems using model-checking. In: Bondavalli, A., Di Giandomenico, F. (eds.) SAFECOMP 2014. LNCS, vol. 8666, pp. 262–277. Springer, Heidelberg (2014)Google Scholar
  18. 18.
    Machin, M., Dufossé, F., Guiochet, J., Powell, D., Roy, M., Waeselynck, H.: Model-checking and game theory for synthesis of safety rules. In: Proceedings of HASE (2015)Google Scholar
  19. 19.
    Martin-Guillerez, D., Guiochet, J., Powell, D., Zanon, C.: A UML-based method for risk analysis of human-robot interactions. In: Proceedings of SERENE, pp. 32–41. ACM (2010)Google Scholar
  20. 20.
    Pradella, M., Morzenti, A., San Pietro, P.: Bounded satisfiability checking of metric temporal logic specifications. ACM TOSEM 22(3), 1–54 (2013)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  • Mehrnoosh Askarpour
    • 1
    Email author
  • Dino Mandrioli
    • 1
  • Matteo Rossi
    • 1
  • Federico Vicentini
    • 2
  1. 1.Dipartimento di Elettronica, Informazione e BioingegneriaPolitecnico di MilanoMilanItaly
  2. 2.Istituto di Tecnologie Industriali e AutomazioneConsiglio Nazionale delle RicercheMilanItaly

Personalised recommendations