Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado Nº 2.242
Aluno: Felipe Augusto da Silva Mendonça
Orientador: Prof. Alexandre Cabral Mota
Coorientador: Dr. Madiel Conserva Filho
Título: Investigando a corretude de um sistema robótico via RoboChart: Um
sistema de distribuição de medicamentos do mundo real
Data: 22/08/2025
Hora/Local: 8h – Virtual – Interessados em assistir entrar em contato com o aluno
Banca Examinadora:
Prof. Gustavo Henrique Porto de Carvalho (UFPE / Centro de Informática)
Prof. Sidney de Carvalho Nogueira (UFRPE / Departamento de Computação)
Prof. Alexandre Cabral Mota (UFPE / Centro de Informática)
RESUMO:
A crescente complexidade dos sistemas de controle em robôs autônomos exige
métodos rigorosos 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 álgebra de
processos CSP. A metodologia proposta inclui a obtenção e abstração do LTS
proveniente da semântica CSP de um modelo RoboChart e a verificação de
conformidade por meio de um algoritmo próprio simplificado de traces
refinement checking, permitindo identificar 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 detecçã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.
Palavras-chave: RoboChart; CSP; Formalização de requisitos; Verificação de
conformidade; Refinamento de Traces.
Comentários desativados