Interoperabilidade entre a biblioteca UnB-DALi e ferramentas UML

Abstract

Uma possível forma de se aferir a dependabilidade de um sistema computacional é por meio de verificação formal de modelos. Esta técnica de verificação de modelos, implementada por ferramentas automáticas como o PRISM (Probabilistic Symbolic Model Checker), requer um modelo devidamente anotado e passível de análise, ou seja, em uma linguagem formal específica. Porém, considerável parte dos sistemas computacionais são modelados em UML, uma linguagem expressa, geralmente, por meio de desenhos, não passíveis de verificação formal. Sendo assim, é necessário transformar um modelo UML para um modelo passível de análise. Oliveira propôs e implementou uma biblioteca Java, a UnB-DALi, que fornece uma API capaz de conduzir essa transformação de forma automática com a ajuda do motor de grafos AGG (Attributed Graph Grammar tool). No entanto, a entrada de dados da UnB-DALi requer uma descrição textual do modelo em código Java, o que não é geralmente feito quando se modela em UML. Porém, várias ferramentas de modelagem UML são capazes de gerar um arquivo textual, em formato XMI, contendo todas as informações dos elementos do diagrama UML. O problema é que este arquivo é proprietário, único de cada ferramenta, e sem a preocupação de aderir aos padrões estabelecidos para arquivos XMI conforme a OMG. Dessa forma, a interoperabilidade dessas ferramentas UML com a biblioteca UnB-DALi pode ser seriamente comprometida. Esta monografia se propõe a fazer a interoperabilidade padronizada entre os arquivos em formatos XMI de diversas ferramentas e a biblioteca UnB-DALi. Para tanto, utilizamos recursos da ferramenta SDMetrics, a qual contém um analisador sintático para XMI. Por fim, avaliamos nossa proposta por meio de testes funcionais definidos em classes de equivalência entre os modelos UML nas ferramentas Papyrus e Astah e seus resultados gerados em PRISM por meio das chamadas à UnB-DALi.