Verificacion Automática del Comportamiento de un Robot Asistente

Abstract

[ES] Los asistentes robóticos autónomos están diseñados para ofrecer compañía a personas que viven en un ambiente doméstico. Este tipo de robot usa diversos sensores para detectar y adaptarse a cualquier imprevisto en el entorno, como evitar obstáculos u otras personas. El desarrollo industrial de los asistentes robóticos carece actualmente de un contexto coherente que pueda asegurar propiedades críticas como su seguridad. Para que los robots asistentes establezcan interacciones avanzadas con humanos de manera segura y confiable, nuevas herramientas y técnicas deben ser desarrolladas para verificar y validar los asistentes robóticos. A fin de lograrlo, en este proyecto nos basamos principalmente en Maude, un lenguaje reflexivo de altas prestaciones diseñado para la especificación formal de sistemas, y en su model checker que, apoyado en la lógica temporal LTL, nos permitirá verificar de manera automática y exhaustiva las propiedades de interés en nuestro modelo de un sistema robótico. Este sistema es el robot asistente Care-O-Bot, dotado de capacidades inteligentes y con una serie de características que deberemos representar en el lenguaje Maude. Posteriormente, aplicando la técnica de model checking se comprobarán diferentes propiedades de alcanzabilidad, seguridad y vivacidad, demostrando de esta forma, con un caso de estudio actual, la potencia y versatilidad de nuestro enfoque.

[CA] Els assistents robòtics autònoms estan dissenyats per oferir companyia a persones que viuen en un ambient domèstic. Aquest tipus de robot utilitza diversos sensors per detectar i adaptar-se a qualsevol imprevist en el entorn, com evitar obstacles o altres persones. El desenvolupament industrial dels assistents robòtics manca actualment d’un context coherent que puga garantir propietats crítiques com és la seguretat. Perquè els robots assistents establisquen interaccions avançades amb humans de manera segura y fiable, noves ferramentes i tècniques han de ser desenvolupades per a verificar i validar els assistents robòtics. A fi de d’aconseguir-ho, en aquest projecte ens basem principalment en Maude, un llenguatge reflexiu d’altes prestacions dissenyat per a l’especificació formal de sistemes, i en el seu model checker que, recolzat en la lògica temporal LTL, ens premetrà verificar de manera automàtica i exhaustiva les propietats d’interés en el nostre model d’un sistema robòtic. Aquest sistema és el robot asistent Care-O-Bot, dotat de capacitats intel·ligents i amb una sèrie de caraterístiques que haurem de representar en el llenguatge Maude. Posteriorment, aplicant la tècnica de model checking es comprovaran diferents propietats d’alcançabilitat, seguretat y vivacitat, demostrant d’aquesta manera, amb un cas d’estudi actual, la potència y versatilitat del nostre enfocament.

[EN] Autonomous robotic assistants are designed to provide companionship for a person living in a typical domestic environment. This type of robot uses several sensors to locate and adapt to any unforeseen in the environment, such as avoiding obstacles or other people. The industrial development of robotic assistants currently lacks a coherent framework that can ensure critical properties such as their safety. For assistant robots to engage in advanced interactions with humans in a trustworthy and safe manner, new tools and techniques must be developed to verify and validate robotic assistants. The aim of this work is to help verify the robot’s behavior by means of an automatic verification tool. This amounts to the design, realisation and evaluation of a model of the robot’s behaviour that is then used as the input model for the automated verifier. First, a model of the robot functionality is specified by a set of control rules that determine how the robot acts in its environment. Then, a model checker will be used to validate the model properties automatically, thus proving the versatility and powerfulness of our approach.