Linguagens e ferramentas utilizadas na especificação formal de software: uma revisão de escopo

Abstract

Este artigo apresenta uma revisão de escopo com o objetivo de identificar as principais linguagens e ferramentas utilizadas na especificação formal de software. A revisão foi realizada em quatro bases de dados (ACM Digital Library, IEEE Xplore, Scopus e Web of Science), utilizando uma string de busca específica e critérios de inclusão e exclusão bem definidos. Após as etapas definidas no protocolo e pesquisa, foram retornados 736 trabalhos na primeira fase, 194 na segunda, 74 na terceira e 17 selecionados para a última fase, onde foram analisados detalhadamente e tiveram suas informações extraídas, verificando-se todos os critérios pré-definidos. Os resultados permitiram identificar as principais linguagens e ferramentas empregadas na especificação formal de software. Revelou-se que a utilização de linguagens formais, ferramentas de verificação e simulação são eficazes para garantir a correta implementação dos requisitos de segurança e para detectar erros em especificações. Além disso, foram discutidos os desafios enfrentados pelas abordagens tradicionais de especificação formal, como a necessidade de habilidades especializadas e a complexidade dos modelos resultantes. Este artigo destaca a importância de tornar as ferramentas de especificação formal mais acessíveis e simplificadas, visando aumentar a adoção e eficácia dessas abordagens.

Keywords

• especificação de software
• métodos formais
• modelagem formal
• validação de software
• verificação formal