Detalhes bibliográficos
| Ano de defesa: |
2012 |
| Autor(a) principal: |
Silva, Rui Carlos Botelho Almeida da |
| Orientador(a): |
Andrade, Aline Maria Santos |
| Banca de defesa: |
Andrade, Aline Mari aSantos,
Silva, Flavio Morais de Assis,
Deharbe, David Boris Paul |
| Tipo de documento: |
Dissertação
|
| Tipo de acesso: |
Acesso aberto |
| Idioma: |
por |
| Instituição de defesa: |
Instituto de Matemática
|
| Programa de Pós-Graduação: |
Programa de Pós-graduação em Mecatrônica
|
| Departamento: |
Não Informado pela instituição
|
| País: |
brasil
|
| Palavras-chave em Português: |
|
| Área do conhecimento CNPq: |
|
| Link de acesso: |
http://repositorio.ufba.br/ri/handle/ri/21342
|
Resumo: |
Os Agentes Autônomos – AA e os Sistemas Multiagentes – SMA realizam suas tarefas baseados num planejamento e a sua complexidade vai depender de qual ambiente esteja envolvido, principalmente quando este ambiente é dinâmico e não determinista. A verificação de modelos tem sido aplicada para a verificação de propriedades do planejamento de modo a checar a correção de aplicações baseadas em AAs e SMA’s e tal verificação apresenta muitos desafios para contornar situações potenciais de explosão de estados. O futebol de robôs simulados é uma aplicação que apresenta muitas das características e problemas inerentes aos AA’s e SMA’s como um ambiente não determinista e dinâmico, fato este que vem tornando esta aplicação um relevante estudo de caso para a verificação de modelos de SMA’s. O presente trabalho considera a especificação e verificação de planos de um time de futebol de robôs simulado, o qual é baseado na arquitetura multicamada de Agentes Concorrentes(camada cognitiva, camada instintiva, e camada reativa), utilizando o verificador de modelos UPPAAL. Para atingir os objetivos do trabalho foi proposta uma abordagem incremental e evolutiva para modelar e verificar os planos, a qual inclui abstrações e técnicas baseadas em verificação composicional de modelos (Compositional Model Checking), com o objetivo de contornar situações de explosão de estados. O método proposto também pode ser utilizado em aplicações similares, o qual poderia ser suportado por um ambiente computacional interativo para guiar os analistas no processo de verificação de planos de SMA’s com arquitetura multicamada, usando a verificação de modelos. |
