Investigando a corretude de um sistema robótico via RoboChart: Um sistema de distribuição de medicamentos do mundo real

Abstract

Acrescente complexidade dos sistemas de controle em robôs autônomos exige métodos ri gorosos para assegurar a conformidade entre especificações e implementações, especialmente em contextos críticos, como a dispensação de medicamentos. Este trabalho apresenta uma abordagem baseada na formalização de requisitos usando RoboChart (uma notação gráfica para a modelagem de sistemas robóticos), que possui uma semântica formal definida na álge bra de processos CSP. A metodologia proposta inclui a obtenção e abstração do LTS proveni ente da semântica CSP de um modelo RoboChart e a verificação de conformidade por meio de um algoritmo próprio simplificado de verificação de refinamento de traces, permitindo identi f icar inconsistências entre especificações formais e implementações práticas desenvolvidas em Python. A abordagem foi aplicada em um sistema robótico de dispensação de medicamentos do Hospital das Clínicas da UFPE (HC-UFPE), desenvolvido no âmbito do projeto CRIAR — Centro de Robótica e Inteligência Artificial Responsável. O sistema integra controle de braço robótico e visão computacional. Os resultados indicam que a abordagem facilita a de tecção de erros e promove um desenvolvimento mais robusto. Como contribuições principais, destacam-se: uma sistemática de formalização de requisitos informais utilizando RoboChart; o desenvolvimento de um algoritmo próprio para verificação de refinamento de traces e a aplicação da metodologia em dois estudos de caso.