Banca de QUALIFICAÇÃO: Danilo José Bispo Galvão
Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.DISCENTE : Danilo José Bispo Galvão
DATA : 05/09/2022
HORA: 08:00
LOCAL: Virtual
TÍTULO:
Uma abordagem para verificação em alto nível de missões multi-robô na UPPAAL
PALAVRAS-CHAVES:
Verificação Formal, Verificação de Modelos, Sistemas Multi-Robô
PÁGINAS: 46
RESUMO:
A necessidade de alavancar meios para especificar missões robóticas a partir de um alto nível de abstração ganhou força devido ao crescimento da popularidade das aplicações robóticas. Como tal, é primordial fornecer meios para garantir que não só a missão robótica seja corretamente especificada, mas que também garanta graus de segurança face à crescente complexidade das tarefas atribuídas aos Sistemas Multi-Robot (MRS). Portanto, as missões do robô agora precisam ser especificadas e verificadas formalmente para robôs e outros agentes envolvidos na operação da missão robótica. No entanto, muitas especificações de missão carecem de um processo de verificação simplificado que garanta que todas as propriedades da missão sejam completamente verificadas por meio da verificação do modelo. Este trabalho propõe um processo de verificação preliminar de modelos para especificação de missão e decomposição de MRS no verificador de modelos UPPAAL. Em particular, apresentamos um modelo semiautomatizado contendo propriedades hierárquicas de definição de domínio transformadas em templates UPPAAL e propriedades de missão formalizadas na linguagem de autômatos temporizados UPPAAL TCTL. No futuro, pretendemos gerar modelos totalmente automaticamente e verificar propriedades de especificação de missão adicionais não cobertas atualmente. Avaliamos nossa abordagem em uma missão robótica de especificação de uma missão logística de alimentos e os resultados mostram que o comportamento esperado é verificado corretamente e as propriedades correspondentes satisfeitas na ferramenta de verificação do modelo UPPAAL.
MEMBROS DA BANCA:
Externo à Instituição - RADU CALINESCU
Presidente - 1720223 - GENAINA NUNES RODRIGUES
Interno - 1848788 - RODRIGO BONIFACIO DE ALMEIDA