A Tecnologia da Informação (TI) fornece suporte às organizações empresariais, proporcionando agilidade e qualidade aos seus processos de negócio. Este suporte é fornecido por aplicações que compõe o ecossistema de software que, de uma maneira geral, não apresenta as características necessárias à integração, dificultando a reutilização. Neste sentido, a Integração de Aplicações Empresariais (EAI) concentra-se na concepção e implementação de soluções de integração. A tecnologia Guaraná DSL é uma das ferramentas que fornecem este suporte, porém, ela difere das outras propostas por incluir um sistema de monitoramento que pode ser configurado usando uma linguagem baseada em regras para gerar soluções com tolerância a falhas. No entanto, Guaraná DSL ainda não está formalizado, e por esta razão, não é possível validar as regras escritas por engenheiros de software utilizando a linguagem baseada em regras. Além disso, não é possível gerar automaticamente as regras com base na semântica de uma solução de integração. Esta pesquisa propõe um estudo detalhado da tecnologia Guaraná DSL com enfase no mecanismo de tolerância a falhas, além do estudo e comparação dos métodos formais: Notação Z, B, Alloy, RSL, Redes de Petri, levando em consideração as características do Guaraná. Utilizando os metamodelos UML com restrições escritas em OCL da linguagem de domínio específico da tecnologia Guaraná encontrados na literatura, foi proposto um modelo matemático com a especificação formal da sintaxe abstrata e posterior validação. Para a especificação formal e validação utilizou-se a Notação Z por meio da ferramenta Z-EVES. / 157 f.