Submitted by Kleber Silva (kleberbs@ufba.br) on 2017-02-06T17:13:39Z
No. of bitstreams: 1
Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-07T12:02:49Z (GMT) No. of bitstreams: 1
Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / Made available in DSpace on 2017-02-07T12:02:49Z (GMT). No. of bitstreams: 1
Rui Carlos Botelho Almeida da Silva.pdf: 4302637 bytes, checksum: 7c1d3de5fed3e9f33254bdc62e656a3a (MD5) / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:192.168.11:11:ri/21342 |
| Date | 09 March 2012 |
| Creators | Silva, Rui Carlos Botelho Almeida da |
| Contributors | Andrade, Aline Maria Santos, Andrade, Aline Mari aSantos, Silva, Flavio Morais de Assis, Deharbe, David Boris Paul |
| Publisher | Instituto de Matemática, Programa de Pós-graduação em Mecatrônica, UFBA, brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFBA, instname:Universidade Federal da Bahia, instacron:UFBA |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0019 seconds