research-article

Open access

Formal modeling and verification of multi-robot interactive scenarios in service settings

Authors:

Livia Lestingi,

Cristian Sbrolli,

Pasquale Scarmozzino,

Marcello M. Bersani,

Matteo RossiAuthors Info & Claims

FormaliSE '22: Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering

Pages 80 - 90

https://doi.org/10.1145/3524482.3527653

Published: 21 July 2022 Publication History

Abstract

Service robots are increasingly widespread in healthcare and domestic assistance settings. Nevertheless, the literature still lacks robotic application development approaches that can deal with the complexity of multi-agent systems and the unpredictability of human behavior. We target this issue by building upon a model-driven development framework for human-robot interactive scenarios that relies on formal analysis (Statistical Model Checking) to estimate the probability of success of the robotic mission. We extend the framework's scope to scenarios featuring multi-robot fleets, a broader range of human-robot interaction contingencies, and task handover between robots. We also present an extended model of human behavior to capture interaction patterns implying close contact or competition with the robot. In the latter case, the user can specify alternative mission plans for the robot, depending on the competition outcome. We illustrate the approach's effectiveness and scalability through a case study from the healthcare setting, featuring multiple mobile robots and humans with diverse physiological characteristics and requesting a broad spectrum of services.

References

[1]

Gul Agha and Karl Palmskog. 2018. A survey of statistical model checking. TOMACS 28, 1 (2018), 1--39.

Digital Library

[2]

Basel Alhaji, Michael Prilla, and Andreas Rausch. 2021. Trust, but Verify: Autonomous Robot Trust Modeling in Human-Robot Collaboration. In Intl. Conf. on Human-Agent Interaction. ACM, Virtual Event, Japan, 402--406.

Digital Library

[3]

Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. 1995. The algorithmic analysis of hybrid systems. TCS 138, 1 (1995), 3--34.

Digital Library

[4]

Marcello M. Bersani, Matteo Soldo, Claudio Menghi, Patrizio Pelliccione, and Matteo Rossi. 2020. PuRSUE - from specification of robotic environments to synthesis of controllers. Formal Aspects Comput. 32, 2--3 (2020), 187--227.

Digital Library

[5]

BlueBotics. 2021. Automated Hospital Logistics: How AGVs are Keeping PPE Moving. https://bluebotics.com/agvs-hospital-logistics/.

[6]

CSKF Calude and N Poznanovic. 2016. Free will is compatible with randomness. Philosophical Inquiries 4, 2 (2016), 37--52.

[7]

Benjamin J. Choi, Ju-Youn Park, and Chung Hyuk Park. 2021. Formal Verification for Human-Robot Interaction in Medical Environments. In Intl. Conf. on Human-Robot Interaction. ACM, Boulder, CO, USA, 181--185.

[8]

Charles J Clopper and Egon S Pearson. 1934. The use of confidence or fiducial limits illustrated in the case of the binomial. Biometrika 26, 4 (1934), 404--413.

[9]

Alexandre David, Kim G Larsen, Axel Legay, Marius Mikučionis, and Danny Bøgsted Poulsen. 2015. Uppaal SMC tutorial. STTT 17, 4 (2015), 397--415.

Digital Library

[10]

Alexandre David, Kim G Larsen, Axel Legay, Marius Mikučionis, Danny Bøgsted Poulsen, Jonas Van Vliet, and Zheng Wang. 2011. Statistical model checking for networks of priced timed automata. In Intl. Conf. on Formal Modeling and Analisys of Timed Systems. Springer, Aalborg, Denmark, 80--96.

[11]

Rocco De Nicola, Luca Di Stefano, and Omar Inverso. 2018. Toward Formal Models and Languages for Verifiable Multi-Robot Systems. Frontiers in Robotics and AI 5 (2018), 94.

[12]

Louise Dennis, Michael Fisher, Marija Slavkovik, and Matt Webster. 2016. Formal verification of ethical choices in autonomous systems. Robotics and Autonomous Systems 77 (2016), 1--14.

Digital Library

[13]

Fatma Faruq, David Parker, Bruno Lacerda, and Nick Hawes. 2018. Simultaneous Task Allocation and Planning Under Uncertainty. In Intl. Conf. on Intelligent Robots and Systems. IEEE, Madrid, Spain, 3559--3564.

[14]

Sergio Feo-Arenis, Milan Vujinović, and Bernd Westphal. 2020. On Implementable Timed Automata. In Intl. Conf. on Formal Techniques for Distributed Objects, Components, and Systems. Springer, Valletta, Malta, 78--95.

[15]

Angelo Ferrando, Louise A. Dennis, Rafael C. Cardoso, Michael Fisher, Davide Ancona, and Viviana Mascardi. 2021. Toward a Holistic Approach to Verification and Validation of Autonomous Cognitive Systems. ACM Trans. Softw. Eng. Methodol. 30, 4 (2021), 43:1--43:43.

Digital Library

[16]

Sergio García, Daniel Strüber, Davide Brugali, Thorsten Berger, and Patrizio Pelliccione. 2020. Robotics software engineering: a perspective from the service robotics domain. In ESEC/FSE. ACM, Virtual Event, USA, 593--604.

[17]

Ulf Grenander. 1950. Stochastic processes and statistical inference. Arkiv för matematik 1, 3 (1950), 195--277.

[18]

Raju Halder, José Proença, Nuno Macedo, and André Santos. 2017. Formal verification of ROS-based robotic applications using timed-automata. In Intl. FME Workshop on Formal Methods in Software Engineering. IEEE, Buenos Aires, Argentina, 44--50.

Digital Library

[19]

ISO 13482. 2014. Robots and robotic devices - Safety requirements for personal care robots. ISO, Geneva, Switzerland.

[20]

Stephan Konz. 2000. Work/rest: Part ii-the scientific basis (knowledge base) for the guide 1. EGPS 1, 401 (2000), 38.

[21]

Hadas Kress-Gazit, Kerstin Eder, Guy Hoffman, Henny Admoni, Brenna Argall, Rudiger Ehlers, Christoffer Heckman, Nils Jansen, Ross A. Knepper, Jan Kretínský, Shelly Levy-Tzedek, Jamy Li, Todd D. Murphey, Laurel D. Riek, and Dorsa Sadigh. 2021. Formalizing and guaranteeing human-robot interaction. Commun. ACM 64, 9 (2021), 78--84.

Digital Library

[22]

Kim G Larsen, Paul Pettersson, and Wang Yi. 1997. UPPAAL in a nutshell. Int. J. on Softw. Tools for Tech. Transf. 1, 1--2 (1997), 134--152.

Digital Library

[23]

Livia Lestingi, Mehrnoosh Askarpour, Marcello M Bersani, and Matteo Rossi. 2020. Formal Verification of Human-Robot Interaction in Healthcare Scenarios. In Software Engineering and Formal Methods. Springer, Amsterdam, The Netherlands, 303--324.

[24]

Livia Lestingi, Mehrnoosh Askarpour, Marcello M Bersani, and Matteo Rossi. 2020. A Model-driven Approach for the Formal Analysis of Human-Robot Interaction Scenarios. In Intl. Conf, on Systems, Man, and Cybernetics. IEEE, Toronto, ON, Canada, 1907--1914.

[25]

Livia Lestingi, Mehrnoosh Askarpour, Marcello M. Bersani, and Matteo Rossi. 2021. A Deployment Framework for Formally Verified Human-Robot Interactions. IEEE Access 9 (2021), 136616--136635.

[26]

Bin Liu, Liang Ma, Chi Chen, and Zhanwu Zhang. 2018. Experimental validation of a subject-specific maximum endurance time model. Ergonomics 61, 6 (2018), 806--817.

[27]

Damian M. Lyons, Ronald C. Arkin, Shu Jiang, Dagan Harrington, Feng Tang, and Peng Tang. 2015. Probabilistic Verification of Multi-robot Missions in Uncertain Environments. In Intl. Conf. on Tools with Artificial Intelligence. IEEE Computer Society, Vietri sul Mare, Italy, 56--63.

[28]

Claudio Menghi, Sergio García, Patrizio Pelliccione, and Jana Tumova. 2018. Towards multi-robot applications planning under uncertainty. In Intl. Conf. on Software Engineering. ACM, Gothenburg, Sweden, 438--439.

Digital Library

[29]

PAL Robotics. 2020. TIAGo Delivery makes an impact in hospitals tackling COVID-19 thanks to DIH-HERO. https://tinyurl.com/muvtr5m8.

[30]

David Porfirio, Allison Sauppé, Aws Albarghouthi, and Bilge Mutlu. 2019. Computational Tools for Human-Robot Interaction Design. In Intl. Conf. on Human-Robot Interaction. IEEE, Daegu, South Korea, 733--735.

[31]

Michael Melholt Quottrup, Thomas Bak, and Roozbeh Izadi-Zamanabadi. 2004. Multi-robot Planning: a Timed Automata Approach. In Intl. Conf. on Robotics and Automation. IEEE, New Orleans, LA, USA, 4417--4422.

[32]

Richard Stocker. 2013. Towards the formal verification of human-agent-robot teamwork. Ph. D. Dissertation. University of Liverpool, UK.

[33]

Charlie Street, Bruno Lacerda, Manuel Mühlig, and Nick Hawes. 2020. Multi-Robot Planning Under Uncertainty with Congestion-Aware Models. In Intl. Conf. on Autonomous Agents and Multiagent Systems. International Foundation for Autonomous Agents and Multiagent Systems, Auckland, New Zealand, 1314--1322.

[34]

Dennis Walter, Holger Täubig, and Christoph Lüth. 2010. Experiences in applying formal verification in robotics. In Intl. Conf. on Computer Safety, Reliability, and Security. Springer, Vienna, Austria, 347--360.

[35]

Matt Webster, David Western, Dejanira Araiza-Illan, Clare Dixon, Kerstin Eder, Michael Fisher, and Anthony G Pipe. 2020. A corroborative approach to verification and validation of human-robot teams. Intl. Journ. of Robotics Research 39, 1 (2020), 73--99.

Digital Library

[36]

N. Yakymets, M. Sango, S. Dhouib, and R. Gelin. 2018. Model-Based Engineering, Safety Analysis and Risk Assessment for Personal Care Robots. In Intl. Conf. on Intelligent Robots and Systems. IEEE, Madrid, Spain, 6136--6141.

Cited By

Kaur J(2024)Synergistic SwarmModeling, Simulation, and Control of AI Robotics and Autonomous Systems10.4018/979-8-3693-1962-8.ch010(166-179)Online publication date: 23-May-2024
https://doi.org/10.4018/979-8-3693-1962-8.ch010
Bersani MCamilli MLestingi LMirandola RRossi MScandurra P(2023)Towards Better Trust in Human-Machine Teaming through Explainable Dependability2023 IEEE 20th International Conference on Software Architecture Companion (ICSA-C)10.1109/ICSA-C57050.2023.00029(86-90)Online publication date: Mar-2023
https://doi.org/10.1109/ICSA-C57050.2023.00029
Bersani MCamilli MLestingi LMirandola RRossi M(2023)Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1109/FormaliSE58978.2023.00010(18-28)Online publication date: May-2023
https://doi.org/10.1109/FormaliSE58978.2023.00010
Show More Cited By

Index Terms

Formal modeling and verification of multi-robot interactive scenarios in service settings

Recommendations

Analyzing the impact of human errors on interactive service robotic scenarios via formal verification
Abstract
Developing robotic applications with human–robot interaction for the service sector raises a plethora of challenges. In these settings, human behavior is essentially unconstrained as they can stray from the plan in numerous ways, constituting a ...
Will you follow the robot's advice?: the impact of robot types and task types on people's perception of a robot
HAI '14: Proceedings of the second international conference on Human-agent interaction

Robots could be classified into an autonomous robot and a tele-operated robot according to the levels of autonomy. As a match between robot types and task types is important, we explored the impact of robot types and task types on social presence, ...
The interactive effects of robot anthropomorphism and robot ability on perceived threat and support for robotics research

The present research examines how a robot's physical anthropomorphism interacts with perceived ability of robots to impact the level of realistic and identity threat that people perceive from robots and how it affects their support for robotics ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

FormaliSE '22: Proceedings of the IEEE/ACM 10th International Conference on Formal Methods in Software Engineering

May 2022

137 pages

ISBN:9781450392877

DOI:10.1145/3524482

General Chairs:
Stefania Gnesi
ISTI-CNR, Italy
,
Nico Plat
Thanos, The Netherlands
,
Program Chairs:
Arnd Hartmanns
University of Twente, The Netherlands
,
Ina Schaefer
Technische Universität Braunschweig, Germany

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering

In-Cooperation

IEEE CS

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 July 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

FormaliSE '22

Sponsor:

SIGSOFT

FormaliSE '22: International Conference on Formal Methods in Software Engineering

May 18 - 22, 2022

Pennsylvania, Pittsburgh

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
414
Total Downloads

Downloads (Last 12 months)215
Downloads (Last 6 weeks)23

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kaur J(2024)Synergistic SwarmModeling, Simulation, and Control of AI Robotics and Autonomous Systems10.4018/979-8-3693-1962-8.ch010(166-179)Online publication date: 23-May-2024
https://doi.org/10.4018/979-8-3693-1962-8.ch010
Bersani MCamilli MLestingi LMirandola RRossi MScandurra P(2023)Towards Better Trust in Human-Machine Teaming through Explainable Dependability2023 IEEE 20th International Conference on Software Architecture Companion (ICSA-C)10.1109/ICSA-C57050.2023.00029(86-90)Online publication date: Mar-2023
https://doi.org/10.1109/ICSA-C57050.2023.00029
Bersani MCamilli MLestingi LMirandola RRossi M(2023)Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning2023 IEEE/ACM 11th International Conference on Formal Methods in Software Engineering (FormaliSE)10.1109/FormaliSE58978.2023.00010(18-28)Online publication date: May-2023
https://doi.org/10.1109/FormaliSE58978.2023.00010
Lestingi LManglaviti AMarinaro DMarinello LAskarpour MBersani MRossi M(2023)Analyzing the impact of human errors on interactive service robotic scenarios via formal verificationSoftware and Systems Modeling (SoSyM)10.1007/s10270-023-01125-123:2(473-502)Online publication date: 17-Aug-2023
https://dl.acm.org/doi/10.1007/s10270-023-01125-1
Bersani MBraghin CGargantini AMirandola RRiccobene EScandurra P(2023)Engineering of Trust Analysis-Driven Digital Twins for a Medical DeviceSoftware Architecture. ECSA 2022 Tracks and Workshops10.1007/978-3-031-36889-9_31(467-482)Online publication date: 16-Jul-2023
https://doi.org/10.1007/978-3-031-36889-9_31

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents