Abstract
Robotic assistants are being designed to help, or work with, humans in a variety of situations from assistance within domestic situations, through medical care, to industrial settings. Whilst robots have been used in industry for some time they are often limited in terms of their range of movement or range of tasks. A new generation of robotic assistants have more freedom to move, and are able to autonomously make decisions and decide between alternatives. For people to adopt such robots they will have to be shown to be both safe and trustworthy. In this paper we focus on formal verification of a set of rules that have been developed to control the Care-O-bot, a robotic assistant located in a typical domestic environment. In particular, we apply model-checking, an automated and exhaustive algorithmic technique, to check whether formal temporal properties are satisfied on all the possible behaviours of the system. We prove a number of properties relating to robot behaviours, their priority and interruptibility, helping to support both safety and trustworthiness of robot behaviours.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E., Grumberg, O., Peled, D.A.: Model Checking. MIT Press (2000)
Duque, I., Dautenhahn, K., Koay, K.L., Willcock, I., Christianson, B.: Knowledge-driven User Activity Recognition for a Smart House. Development and Validation of a Generic and Low-Cost, Resource-Efficient System. In: Proc. of the Sixth Int. Conf. on Advances in Computer-Human Interactions (ACHI), pp. 141–146 (2013)
Fainekos, G., Kress-Gazit, H., Pappas, G.: Temporal Logic Motion Planning for Mobile Robots. In: Proceedings of the IEEE International Conference on Robotics and Automation (ICRA), pp. 2020–2025. IEEE Computer Society Press (2005)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2003)
Kim, M., Kang, K.C.: Formal construction and verification of home service robots: A case study. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 429–443. Springer, Heidelberg (2005)
Kouskoulas, Y., Renshaw, D., Platzer, A., Kazanzides, P.: Certifying the safe design of a virtual fixture control algorithm for a surgical robot. In: Proc. of the 16th Int. Conf. on Hybrid Systems: Computation and Control, pp. 263–272. ACM (2013)
Mohammed, A., Furbach, U., Stolzenburg, F.: Multi-Robot Systems: Modeling, Specification, and Model Checking, ch. 11, pp. 241–265. InTechOpen (2010)
Proetzsch, M., Berns, K., Schuele, T., Schneider, K.: Formal Verification of Safety Behaviours of the Outdoor Robot RAVON. In: Fourth Int. Conf. on Informatics in Control, Automation and Robotics (ICINCO), pp. 157–164. INSTICC Press (2007)
Reiser, U., Connette, C.P., Fischer, J., Kubacki, J., Bubeck, A., Weisshardt, F., Jacobs, T., Parlitz, C., Hägele, M., Verl, A.: Care-o-bot®3 - creating a product vision for service robot applications by integrating design and technology. In: IEEE/RSJ Int. Conf. on Intelligent Robots and Systems (IROS), pp. 1992–1998 (2009)
Saunders, J., Burke, N., Koay, K.L., Dautenhahn, K.: A user friendly robot architecture for re-ablement and co-learning in a sensorised home. In: Assistive Technology: From Research to Practice (Proc. of AAATE), vol. 33, pp. 49–58 (2013)
Saunders, J., Salem, M., Dautenhahn, K.: Temporal issues in teaching robot behaviours in a knowledge-based sensorised home. In: Proc. 2nd International Workshop on Adaptive Robotic Ecologies (2013)
Saunders, J., Syrdal, D.S., Dautenhahn, K.: A template based user teaching system for an assistive robot. In: Proceedings of 3rd International Symposium on New Frontiers in Human Robot Interaction at AISB 2014 (2014)
Sierhuis, M., Clancey, W.J.: Modeling and simulating work practice: A method for work systems design. IEEE Intelligent Systems 17(5), 32–41 (2002)
Stocker, R., Dennis, L., Dixon, C., Fisher, M.: Verifying Brahms Human-Robot Teamwork Models. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds.) JELIA 2012. LNCS, vol. 7519, pp. 385–397. Springer, Heidelberg (2012)
Syrdal, D.S., Dautenhahn, K., Koay, K.L., Walters, M.L., Ho, W.C.: Sharing spaces, sharing lives–the impact of robot mobility on user perception of a home companion robot. In: Proc. of 5th Int. Conf. on Social Robotics (ICSR), pp. 321–330 (2013)
Walter, D., Täubig, H., Lüth, C.: Experiences in applying formal verification in robotics. In: Schoitsch, E. (ed.) SAFECOMP 2010. LNCS, vol. 6351, pp. 347–360. Springer, Heidelberg (2010)
Webster, M., Dixon, C., Fisher, M., Salem, M., Saunders, J., Koay, K.L., Dautenhahn, K.: Formal verification of an autonomous personal robotic assistant. In: Proc. of Workshop on Formal Verification and Modeling in Human-Machine Systems (FVHMS), pp. 74–79. AAAI (2014)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Dixon, C., Webster, M., Saunders, J., Fisher, M., Dautenhahn, K. (2014). “The Fridge Door is Open”–Temporal Verification of a Robotic Assistant’s Behaviours. In: Mistry, M., Leonardis, A., Witkowski, M., Melhuish, C. (eds) Advances in Autonomous Robotics Systems. TAROS 2014. Lecture Notes in Computer Science(), vol 8717. Springer, Cham. https://doi.org/10.1007/978-3-319-10401-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-10401-0_9
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10400-3
Online ISBN: 978-3-319-10401-0
eBook Packages: Computer ScienceComputer Science (R0)