UnB-DALi : biblioteca para transformação de modelos em análise de dependabilidade

Abstract

Métodos para a engenharia e análise de Sistemas Críticos precisam lidar constantemente com Transformações de Modelos, dado que a maioria desses sistemas são desenvolvidos seguindo uma abordadem modelo-dirigida. Essa asserção é especialmente válida para uma análise de dependabilidade desses sistemas via Verificação de Modelos UML, onde modelos UML precisam ser transformados em modelos passíveis de Model Checking por uma ferramenta apropriada. Várias são as técnicas existentes que automatizam tais transformações, mas a maioria delas carece de interoperabilidade, reusabilidade e rigorosidade matemática. Dito isso, nessa monografia é apresentado e elaborado a arquitetura e implementação do UnB-DALi, uma biblioteca Java que conduz a transformação de modelos comportamentais UML anotados para modelos DTMCs na notação da ferramenta PRISM. As transformações são baseadas na sintaxe abstrata inerente a esses modelos, seus grafos subjacentes, construção possível via formalismo matemático de Transformação de Grafos Tipados e Atributados, apropriadamente implementado pela ferramenta AGG. Ao final desta monografia, experimentos foram conduzidos para atestar parcialmente a validade do que foi implementado.