https://repositorio.ufba.br/handle/ri/18477
Tipo: | Dissertação |
Título: | Tangram: uma ferramenta de apoio à verificação formal de sistemas de tempo real baseados em componentes |
Autor(es): | Muniz, André Luís Nunes |
Autor(es): | Muniz, André Luís Nunes |
Abstract: | 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. |
Palavras-chave: | Projeto de sistemas Software - componentes UML (Computação) Sistemas de computação |
País: | brasil |
Sigla da Instituição: | UFBA |
metadata.dc.publisher.program: | Mecatrônica |
Tipo de Acesso: | Acesso Aberto |
URI: | http://repositorio.ufba.br/ri/handle/ri/18477 |
Data do documento: | 14-Jan-2016 |
Aparece nas coleções: | Dissertação (PPGM) |
Arquivo | Descrição | Tamanho | Formato | |
---|---|---|---|---|
Dissertação-André-Muniz.pdf | 3,31 MB | Adobe PDF | Visualizar/Abrir |
Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.