Submitted by LIVIA FREITAS (livia.freitas@ufba.br) on 2016-01-07T15:22:21Z
No. of bitstreams: 1
Dissertação-André-Muniz.pdf: 3386047 bytes, checksum: b3c92a5e3dbc8813fb07b262694fd7f0 (MD5) / Approved for entry into archive by LIVIA FREITAS (livia.freitas@ufba.br) on 2016-01-14T17:47:44Z (GMT) No. of bitstreams: 1
Dissertação-André-Muniz.pdf: 3386047 bytes, checksum: b3c92a5e3dbc8813fb07b262694fd7f0 (MD5) / Made available in DSpace on 2016-01-14T17:47:44Z (GMT). No. of bitstreams: 1
Dissertação-André-Muniz.pdf: 3386047 bytes, checksum: b3c92a5e3dbc8813fb07b262694fd7f0 (MD5) / 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:192.168.11:11:ri/18477 |
| Date | 30 October 2009 |
| Creators | Muniz, André Luís Nunes |
| Contributors | Andrade, Aline Maria Santos, Lima, George Marconi de Araújo, Andrade, Aline Maria Santos, Farines, Jean-Marie, Macêdo, Raimundo José de Araújo |
| Publisher | Universidade Federal da Bahia. Escola Politécnica/Instituto de Matemática, 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.0013 seconds