Por favor, use este identificador para citar o enlazar este ítem:
https://repositorio.ufba.br/handle/ri/18477
metadata.dc.type: | Dissertação |
Título : | Tangram: uma ferramenta de apoio à verificação formal de sistemas de tempo real baseados em componentes |
Autor : | Muniz, André Luís Nunes |
metadata.dc.creator: | Muniz, André Luís Nunes |
Resumen : | Sistemas computacionais são utilizados atualmente em aplicações consideradas criticas e com alto grau de complexidade, como e o exemplo da automação industrial, controle de navegação em aeronaves, equipamentos médicos, entre outros. Com o intuito de lidar com esta complexidade e, ao mesmo tempo, dar garantias de confiabilidade, novas abordagens de desenvolvimento e validação de software t^em sido empregadas neste contexto. No que tange os chamados sistemas de tempo real, nos quais a correção do sistema depende do cumprimento de suas restrições temporais, duas abordagens vem ganhando muita atenção nos últimos anos, o desenvolvimento baseado em componentes, ou CBD (Component-Based Development), e os métodos formais de verificação de software, com atenção especial para a verificação de modelos (Model-Checking), que esta entre as técnicas formais mais utilizadas na industria e na academia. Entretanto, existem poucas abordagens propostas no sentido de aplicar a verificacao de modelos a sistemas de tempo real críticos baseados em componentes. Um dos principais desa os nesta área e a falta de abordagens/ferramentas que deem suporte a uma fácil integração dos métodos formais ao processo de desenvolvimento baseado em componentes. Isto e causado muitas vezes pela falta de compatibilidade entre as abordagens atuais de verificação formal e os diversos modelos de componentes existentes no mercado. Diante disto, este trabalho propõe uma abordagem para a integração da verificação de modelos ao processo de desenvolvimento baseado em componentes para sistemas de tempo real, através de uma tradução automática de modelos semi-formais de sistemas baseados em componentes para modelos formais passiveis de verificação. A linguagem de modelagem considerada neste trabalho e a UML (Uni ed Modeling Language), a qual ja e um padrão em termos de especificação de sistemas, sendo largamente utilizada na industria e na academia, para diversos tipos de aplicação e abordagens de desenvolvimento. Os modelos formais gerados pela tradução são autômatos temporizados do verificador de modelos UPPAAL, o qual e um verificador de modelos voltado para sistemas de tempo real. Para dar suporte a abordagem deste trabalho, foi desenvolvida uma ferramenta chamada TANGRAM (Tool for Analysis of Diagrams), a qual e capaz de traduzir diagramas da UML em automatos temporizados. Um estudo de caso da utilizacao de TANGRAM foi realizado e e apresentado neste trabalho. |
Palabras clave : | Projeto de sistemas Software - componentes UML (Computação) Sistemas de computação |
metadata.dc.publisher.country: | brasil |
metadata.dc.publisher.initials: | UFBA |
metadata.dc.publisher.program: | Mecatrônica |
metadata.dc.rights: | Acesso Aberto |
URI : | http://repositorio.ufba.br/ri/handle/ri/18477 |
Fecha de publicación : | 14-ene-2016 |
Aparece en las colecciones: | Dissertação (PPGM) |
Ficheros en este ítem:
Fichero | Descripción | Tamaño | Formato | |
---|---|---|---|---|
Dissertação-André-Muniz.pdf | 3,31 MB | Adobe PDF | Visualizar/Abrir |
Los ítems de DSpace están protegidos por copyright, con todos los derechos reservados, a menos que se indique lo contrario.