Resumo:
Um dos primeiros passos em um processo de desenvolvimento de um software é o processo
de modelagem, onde são levantados requisitos e feito os modelos que servirão de base para
todo o decorrer do projeto. Porém, muitas vezes estes modelos são criados de forma
inconsistente ou ambígua, causando problemas no decorrer do processo de desenvolvimento,
obrigando os desenvolvedores a voltarem para a etapa de análise, para alterar novamente o
modelo, causando assim um impacto negativo nos custos e prazos do projeto. Assim, este
trabalho possui como objetivo principal o desenvolvimento de uma ferramenta de
modelagem, na qual o analista possa desenhar um diagrama de classe e as inconsistências e
ambiguidades dele já possam ser verificadas e corrigidas ainda no processo de análise por
meio do seu mapeamento para a linguagem formal Event-B.
