http://repositorio.unb.br/handle/10482/49798| Arquivo | Tamanho | Formato | |
|---|---|---|---|
| DaniloJoseBispoGalvao_DISSERT.pdf | 2,67 MB | Adobe PDF | Visualizar/Abrir |
| Título: | Uma abordagem para verificação de missões multi-robôs em alto nível no UPPAAL |
| Outros títulos: | An approach for high-level multi-robot mission verification in UPPAAL |
| Autor(es): | Galvão, Danilo José Bispo |
| Orientador(es): | Rodrigues, Genaína Nunes |
| Assunto: | Verificação formal Verificação de modelos Sistemas Multi-Robô |
| Data de publicação: | 13-Ago-2024 |
| Data de defesa: | 31-Jan-2023 |
| Referência: | GALVÃO, Danilo José Bispo. Uma abordagem para verificação de missões multi-robôs em alto nível no UPPAAL. 2023. 98 f., il. Dissertação (Mestrado em Informática) — Universidade de Brasília, Brasília, 2023. |
| Abstract: | The need to leverage means to specify robotic missions from a high abstraction level has gained momentum due to the popularity growth of robotic applications. As such, it is paramount to provide means to guarantee that not only the robotic mission is correctly specified, but that it also guarantees degrees of safety given the growing complexity of tasks assigned to Multi-Robot System (MRS). Therefore, robot missions now need to be specified and formally verified for both robots and other agents involved in the robotic mission operation. However, many mission specifications lack a streamlined verification process that ensures that all mission properties are thoroughly verified through model checking. This work proposes a model checking process for mission specification and decomposition of MRS in Uppaal model checker. In particular, we present an automated generation process containing hierarchical domain definition properties transformed into Uppaal templates and mission properties formalized into the Uppaal timed automata language TCTL. We have evaluated our approach in three robotic missions and results show that the expected behaviour is correctly verified and the corresponding properties satisfied in the Uppaal model checking tool. |
| Unidade Acadêmica: | Instituto de Ciências Exatas (IE) Departamento de Ciência da Computação (IE CIC) |
| Informações adicionais: | Dissertação (Mestrado) — Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2023. |
| Programa de pós-graduação: | Programa de Pós-Graduação em Informática |
| Licença: | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.unb.br, www.ibict.br, www.ndltd.org sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra supracitada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data. |
| Agência financiadora: | Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES). |
| Aparece nas coleções: | Teses, dissertações e produtos pós-doutorado |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.