Formalização e verificação de modelos de estilo arquitetural de software

Neste estudo modelos formais do sistema ATM são descritos usando linguagens baseadas em estados como Z B e Alloy bem como linguagens baseadas em eventos como Monterey Phoenix. A verificação de modelos está a ser realizada por ferramentas automatizadas a saber Z/EVES Atelier B e Alloy Analyzer para especificações Z B e Alloy respetivamente. Além disso foi apresentada uma análise comparativa das diferentes características apresentadas por várias abordagens formais. A arquitetura de software desempenha um papel importante no design de alto nível de um sistema em termos de componentes conectores e configurações. O principal elemento constitutivo da arquitetura de software é um estilo arquitetónico que fornece semântica de design específica do domínio. Na análise de estilos arquitetónicos complexos foi feita uma tentativa no nosso trabalho de formalizar um estilo complexo por exemplo C2 (componente e conector) utilizando a linguagem de especificação formal Alloy. Para a verificação da consistência das notações de modelagem é utilizada a ferramenta de verificação de modelos por exemplo Alloy Analyzer.