Tangram: uma ferramenta de apoio à verificação formal de sistemas de tempo real baseados em componentes

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.