Campo DC | Valor | Idioma |
dc.contributor.advisor | Andrade, Aline Maria Santos | - |
dc.contributor.author | Muniz, André Luís Nunes | - |
dc.creator | Muniz, André Luís Nunes | - |
dc.date.accessioned | 2016-01-14T17:47:44Z | - |
dc.date.available | 2016-01-14T17:47:44Z | - |
dc.date.issued | 2016-01-14 | - |
dc.date.submitted | 2009-10-30 | - |
dc.identifier.uri | http://repositorio.ufba.br/ri/handle/ri/18477 | - |
dc.description.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. | pt_BR |
dc.language.iso | pt_BR | pt_BR |
dc.rights | Acesso Aberto | pt_BR |
dc.subject | Projeto de sistemas | pt_BR |
dc.subject | Software - componentes | pt_BR |
dc.subject | UML (Computação) | pt_BR |
dc.subject | Sistemas de computação | pt_BR |
dc.title | Tangram: uma ferramenta de apoio à verificação formal de sistemas de tempo real baseados em componentes | pt_BR |
dc.type | Dissertação | pt_BR |
dc.contributor.advisor-co | Lima, George Marconi de Araújo | - |
dc.contributor.referees | Andrade, Aline Maria Santos | - |
dc.contributor.referees | Farines, Jean-Marie | - |
dc.contributor.referees | Macêdo, Raimundo José de Araújo | - |
dc.publisher.departament | Universidade Federal da Bahia. Escola Politécnica/Instituto de Matemática | pt_BR |
dc.publisher.program | Mecatrônica | pt_BR |
dc.publisher.initials | UFBA | pt_BR |
dc.publisher.country | brasil | pt_BR |
Aparece nas coleções: | Dissertação (PPGM)
|