Enriching SysML-based software architecture descriptions: a model-driven approach

• Ano de defesa: 2023
• Autor(a) principal: Araújo, Camila de
• Orientador(a): Batista, Thais Vasconcelos
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Rio Grande do Norte
• Programa de Pós-Graduação: PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
• País: Brasil
• Palavras-chave em Português: Computação; Software architecture; Architectural description language; Model-driven development; Formal verification; SysADL; Pi-ADL
• Área do conhecimento CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
• Link de acesso: https://repositorio.ufrn.br/handle/123456789/53351

A natureza crítica de muitos sistemas complexos de uso intensivo de software requer descrições formais de arquitetura para dar suporte à análise arquitetural automatizada em relação às propriedades de correção. Devido aos desafios de adotar abordagens formais, muitos arquitetos têm preferido usar notações como UML, SysML e seus derivados para descrever a estrutura e o comportamento das arquiteturas de software. No entanto, essas notações semi-formais têm limitações quanto ao suporte à análise arquitetural, principalmente à verificação formal. Este trabalho investiga como oferecer suporte formal a descrições de arquitetura baseadas em SysML para permitir a verificação formal de arquiteturas de software. Como resultado desta pesquisa, a principal contribuição é propor uma abordagem orientada a modelos (MDD) que fornece semântica formal para uma linguagem de arquitetura baseada em SysML, SysADL, por meio de uma transformação contínua das descrições da arquitetura SysADL para as especificações formais correspondentes em p-ADL, uma linguagem teoricamente bem fundamentada baseada no p-calculus de tipo de ordem superior. A implementação da proposta envolve a execução de um processo de 4 fases: (i) transformação modelo-a-modelo (M2M) de modelos SysADL em modelo p-ADL; (ii) transformação de modelo para texto (M2T) de modelos p-ADL em código p-ADL; (iii) geração de arquitetura executável correspondente e validação da arquitetura; e (iv) verificação de propriedades. O trabalho tem outras contribuições associadas para dar suporte ao processo de 4 fases: (i) uma semântica denotacional para SysADL; (ii) a definição de um processo para suportar a transformação automatizada de modelos SysADL em modelos p-ADL; (iii) A validação da arquitetura p-ADL gerada pela transformação MDD para mostrar que está de acordo com a arquitetura original SysADL; e (iv) a verificação de propriedades arquiteturais formais usando rastros de execução. A proposta foi implementada e validada utilizando uma arquitetura de Sistema de Monitoramento de Enchentes.