FormAr: software architecture formalization for critical applications

Detalhes bibliográficos
Ano de defesa: 2022
Autor(a) principal: Dias, Fagner Morais
Orientador(a): Oliveira, Marcel Vinicius Medeiros
Banca de defesa: Não Informado pela instituição
Tipo de documento: Dissertação
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
Departamento: Não Informado pela instituição
País: Brasil
Palavras-chave em Português:
CSP
Link de acesso: https://repositorio.ufrn.br/handle/123456789/47091
Resumo: Erros durante o desenvolvimento do software podem originar falhas no sis- tema que podem causar danos importantes. Uma das etapas mais importantes no processo de desenvolvimento de software é a modelagem da arquitetura do sistema, possivelmente usando linguagens de descrição de arquitetura de software (ADLs). As ADLs atualmente adotadas pela indústria para sistemas intensivos de software são em sua maioria semiformais e essencialmente base- adas em SysML e perfis especializados. Essas ADLs permitem descrever a estrutura e o comportamento do sistema. Além disso, é possível gerar modelos executáveis ou gerar código em uma linguagem de programação alvo e simular seu comportamento. Isso, no entanto, não constitui prova de que o sistema está correto ou seguro. Este trabalho propõe uma nova abordagem para capacitar ADLs baseadas em SysML com verificação formal suportada por verificação de modelo. Ele apresenta uma semântica baseada em CSP para modelos SysADL. Além disso, este trabalho apresenta como as propriedades de correção podem ser formalmente especificadas usando CSP, e como o verificador de refinamento de modelos FDR4 pode verificar essas propriedades de correção. Finalmente, apresentamos a nova extensão do SysADL studio que permite a transformação automatizada de descrições de arquitetura SysADL para processos CSP e a verificação de propriedades importantes de correção do sistema. Toda a abordagem é ilustrada por meio de um estudo de caso, que também faz parte deste documento. Este estudo de caso demonstra a utilidade de nossa abordagem na prática.