Formalização do diagrama do casos de uso por meio da linguagem Event-B

Abstract

A Unified Modeling Language é um padrão de modelagem orientada a objetos bastante aceito e utilizado no desenvolvimento de sistemas. Entretanto, ela não garante a consistência de seus modelos por permitir múltiplas interpretações deles, o que causa inúmeros erros durante o desenvolvimento, que por sua vez impacta nos custos e prazos do projeto. Este trabalho tem como objetivo proporcionar um mecanismo para verificação do Diagrama de Casos de Uso proposto pelo Iconix através de uma ferramenta CASE que, além de proporcionar a criação e edição do diagrama, permita a sua transformação para a linguagem formal Event-B.