Document Open Access Logo

Verifying Autonomous Robots: Challenges and Reflections (Invited Talk)

Author Clare Dixon

PDF
Thumbnail PDF

File

LIPIcs.TIME.2020.1.pdf
  • Filesize: 278 kB
  • 4 pages

Document Identifiers

Author Details

Clare Dixon
  • Department of Computer Science, The University of Manchester, UK

Funding

  • Dixon, Clare: This work was funded by the Engineering and Physical Sciences Research Council (EPSRC) under the grants Trustworthy Robot Systems (EP/K006193/1) and Science of Sensor Systems Software (S4 EP/N007565/1) and by the UK Industrial Strategy Challenge Fund (ISCF), delivered by UKRI and managed by EPSRC under the grants Future AI and Robotics Hub for Space (FAIR-SPACE EP/R026092/1) and Robotics and Artificial Intelligence for Nuclear (RAIN EP/R026084/1).

Acknowledgements

The work discussed in this document was carried out collaboratively with researchers on the following funded research projects: Trustworthy Robot Systems; Science of Sensor Systems Software; Future AI and Robotics Hub for Space; and Robotics and Artificial Intelligence for Nuclear.

Cite As Get BibTex

Clare Dixon. Verifying Autonomous Robots: Challenges and Reflections (Invited Talk). In 27th International Symposium on Temporal Representation and Reasoning (TIME 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 178, pp. 1:1-1:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.TIME.2020.1

Abstract

Autonomous robots such as robot assistants, healthcare robots, industrial robots, autonomous vehicles etc. are being developed to carry out a range of tasks in different environments. The robots need to be able to act autonomously, choosing between a range of activities. They may be operating close to or in collaboration with humans, or in environments hazardous to humans where the robot is hard to reach if it malfunctions. We need to ensure that such robots are reliable, safe and trustworthy. In this talk I will discuss experiences from several projects in developing and applying verification techniques to autonomous robotic systems. In particular we consider: a robot assistant in a domestic house, a robot co-worker for a cooperative manufacturing task, multiple robot systems and robots operating in hazardous environments.

Subject Classification

ACM Subject Classification
  • Computer systems organization → Dependable and fault-tolerant systems and networks
  • Software and its engineering → Software verification and validation
  • Theory of computation → Logic
Keywords
  • Verification
  • Autonomous Robots

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. D. Araiza-Illan, D. Western, A. G. Pipe, and K. Eder. Coverage-driven verification - an approach to verify code for robots that directly interact with humans. In N. Piterman, editor, Hardware and Software: Verification and Testing - 11th International Haifa Verification Conference, HVC 2015, Haifa, Israel, November 17-19, 2015, Proceedings, volume 9434 of Lecture Notes in Computer Science, pages 69-84. Springer, 2015. Google Scholar
  2. R. C. Cardoso, M. Farrell, M. Luckcuck, A. Ferrando, and M. Fisher. Heterogeneous verification of an autonomous curiosity rover. In Proceedings of the NASA Formal Methods Symposium. Springer, 2020. Google Scholar
  3. A. Cimatti, E. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tacchella. NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of LNCS, Copenhagen, Denmark, July 2002. Springer. Google Scholar
  4. E. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 2000. Google Scholar
  5. C. Dixon, M. Webster, J. Saunders, M. Fisher, and K. Dautenhahn. "The Fridge Door is Open"-Temporal Verification of a Robotic Assistant’s Behaviours. In M. Mistry, A. Leonardis, M. Witkowski, and C. Melhuish, editors, Advances in Autonomous Robotics Systems, volume 8717 of Lecture Notes in Computer Science, pages 97-108. Springer, 2014. Google Scholar
  6. C. Dixon, A.F.T. Winfield, M. Fisher, and C. Zeng. Towards Temporal Verification of Swarm Robotic Systems. Robotics and Autonomous Systems, 2012. Google Scholar
  7. M. Farrell, R. C. Cardoso, L. A. Dennis, C. Dixon, M. Fisher, G. Kourtis, A. Lisitsa, M. Luckcuck, and M. Webster. Modular verification of autonomous space robotics. In Assurance of Autonomy for Robotic Space Missions Workshop, 2019. Google Scholar
  8. M. Fisher. An Introduction to Practical Formal Methods Using Temporal Logic. Wiley, 2011. Google Scholar
  9. P. Gainer, C. Dixon, K. Dautenhahn, M. Fisher, U. Hustadt, J. Saunders, and M. Webster. Cruton: Automatic verification of a robotic assistant’s behaviours. In L. Petrucci, C. Seceleanu, and A. Cavalcanti, editors, Critical Systems: Formal Methods and Automated Verification, Proceedings of FMICS-AVoCS, volume 10471 of Lecture Notes in Computer Science, pages 119-133. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-67113-0_8.
  10. P. Gainer, S. Linker, C. Dixon, U. Hustadt, and M. Fisher. Multi-Scale Verification of Distributed Synchronisation. Formal Methods in System Design, 2020. Google Scholar
  11. A. Hinton, M. Kwiatkowska, G. Norman, and D. Parker. PRISM: A Tool for Automatic Verification of Probabilistic Systems. In Proc. 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 3920 of LNCS, pages 441-444. Springer, 2006. Google Scholar
  12. G. J. Holzmann. The SPIN Model Checker. Addison-Wesley, 2003. Google Scholar
  13. S. Konur, C. Dixon, and M. Fisher. Analysing Robot Swarm Behaviour via Probabilistic Model Checking. Robotics and Autonomous Systems, 60(2):199-213, 2012. Google Scholar
  14. M. Luckcuck, M. Farrell, L. A. Dennis, C. Dixon, and M. Fisher. Formal specification and verification of autonomous robotic systems: A survey. ACM Computing Surveys, 52(5), 2019. Google Scholar
  15. M. Salem, G. Lakatos, F. Amirabdollahian, and K. Dautenhahn. Would You Trust a (Faulty) Robot?: Effects of Error, Task Type and Personality on Human-Robot Cooperation and Trust. In International Conference on Human-Robot Interaction (HRI), pages 141-148, Portland, Oregon, USA, 2015. ACM/IEEE. Google Scholar
  16. J. Saunders, N. Burke, K. L. Koay, and K. Dautenhahn. A User Friendly Robot Architecture for Re-ablement and Co-learning in A Sensorised Home. In European AAATE (Associated for the Advancement of Assistive Technology in Europe) Conference, Vilamoura, Portugal, 2013. Google Scholar
  17. M. Sierhuis, W. J. Clancey, and R. J. J. van Hoof. Brahms an agent-oriented language for work practice simulation and multi-agent systems development. In R. H. Bordini, M. Dastani, J. Dix, and A. El Fallah-Seghrouchni, editors, Multi-Agent Programming, Languages, Tools and Applications, pages 73-117. Springer, 2009. Google Scholar
  18. M. Webster, M. Breza, C. Dixon, M. Fisher, and J. McCann. Exploring the effects of environmental conditions and design choices on IOT systems using formal methods. Journal of Computational Science, 2020. Google Scholar
  19. M. Webster, C. Dixon, M. Fisher, M. Salem, J. Saunders, K. Koay, and K. Dautenhahn. Formal verification of an autonomous personal robotic assistant. In Proceedings of Workshop on Formal Verification in Human Machine Systems (FVHMS). AAAI, 2014. Google Scholar
  20. M. Webster, C. Dixon, M. Fisher, M. Salem, J. Saunders, K. L. Koay, K. Dautenhahn, and J. Saez-Pons. Toward Reliable Autonomous Robotic Assistants Through Formal Verification: A Case Study. IEEE Transactions on Human-Machine Systems, 46(2):186-196, April 2016. Google Scholar
  21. M. Webster, D. Western, D. Araiza-Illan, C. Dixon, K. Eder, M. Fisher, and A. Pipe. A corroborative approach to verification and validation of human-robot teams. International Journal of Robotics Research, 39(1):73-99, 2020. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact