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

Caio Alberto Nunes Marques

ORCID iD Universidade Federal Rural do Semi-Árido (UFERSA), Pau dos Ferros, Rio Grande do Norte, Brasil

Maria Adriana Ferreira da Silva

ORCID iD Universidade Federal Rural do Semi-Árido (UFERSA), Pau dos Ferros, Rio Grande do Norte, Brasil

José Lucas Santana de Andrade

ORCID iD Universidade Federal Rural do Semi-Árido (UFERSA), Pau dos Ferros, Rio Grande do Norte, Brasil

Alysson Filgueira Milanez

ORCID iD Universidade Federal Rural do Semi-Árido (UFERSA), Pau dos Ferros, Rio Grande do Norte, Brasil

Resumo

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.

Palavras-chave


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


Texto completo:

Referências


APVRILLE, L.; SAQUI-SANNES, P.; VINGERHOEDS, R. An educational case study of using SysML and TTool for unmanned aerial vehicles design. IEEE Journal on Miniaturization for Air and Space Systems, v. 1, n. 2, p. 117-129, 2020. DOI: https://doi.org/10.1109/JMASS.2020.3013325.

ARKSEY, H.; O’MALLEY, L. Scoping studies: towards a methodological framework. International Journal of Social Research Methodology, v. 8, n. 1, p. 19-32, 2005. DOI: https://doi.org/10.1080/1364557032000119616.

ATOUM, I.; BAKLIZI, M. K.; ALSMADI, I.; OTOOM, A. A.; ALHERSH, T.; ABABNEH, J.; ALMALKI, J.; ALSHAHRANI, S. M. Challenges of software requirements quality assurance and validation: a systematic literature review. IEEE Access, v. 9, p. 137613-137634, 2021. DOI: https://doi.org/10.1109/ACCESS.2021.3117989.

BERNHARDT, G. H.; PFIZ, F. S.; HO, S. L.; RODRIGUES, J. P. L.; ZANINI, E. O. A utilização da linguagem de modelagem unificada (UML) na engenharia de software: uma avaliação da adoção e relevância. In: ENCONTRO CIENTÍFICO CULTURAL INTERINSTITUCIONAL, 21., Cascavel, 2023. Anais [...]. Cascavel: FAG, 2023. Disponível em: https://www4.fag.edu.br/anais-2023/Anais-2023-48.pdf. Acesso em: 12 ago. 2024.

BRIDA, S. G.; REGIS, G.; ZHENG, G.; BAGHERI, H.; NGUYEN, T.-V.; AGUIRRE, N.; FRIAS, M. Artifact of bounded exhaustive search of alloy specification repairs. In: 2021 IEEE/ACM INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: COMPANION PROCEEDINGS (ICSE-COMPANION), 43., 2021, Madrid. Proceedings […]. Madrid: IEEE, p. 209-210, 2021. DOI: https://doi.org/10.1109/ICSE-Companion52605.2021.00093.

CARDENAS, H.; ZIMMERMAN, R.; VIESCA, A. R.; AL LAIL, M.; PEREZ, A. J. Formal UML-based modeling and analysis for securing location-based IoT applications. In: IEEE INTERNATIONAL CONFERENCE ON MOBILE AD HOC AND SMART SYSTEMS (MASS), 19., 2022, Denver. Proceedings […]. Denver: IEEE, 2022, p. 722-723. DOI: https://doi.org/10.1109/MASS56207.2022.00109.

FERRARI, A.; BEEK, M. H. T. Formal methods in railways: a systematic mapping study. ACM Computing Surveys, v. 55, n. 4, p. 1-37, 2023. DOI: https://doi.org/10.1145/3520480.

HALCHIN, A.; AIT-AMEUR, Y.; SINGH, N. K.; FELIACHI, A.; ORDIONI, J. Certified embedding of B models in an integrated verification framework. In: 2019 INTERNATIONAL SYMPOSIUM ON THEORETICAL ASPECTS OF SOFTWARE ENGINEERING (TASE), 2019, Guilin. Proceedings […]. Guilin: IEEE, 019. p. 168-175. DOI: https://doi.org/10.1109/TASE.2019.000-4.

HILKEN, F.; HAMANN, L. History of the USE tool 20 Years of UML/OCL modeling made in Germany. JOT – The Journal of Object Technology, v. 19, n. 3, p. 3:1-13, 2020. DOI: http://dx.doi.org/10.5381/jot.2020.19.3.a20.

KHAN, W.; KAMRAN, M.; AHMAD, A.; KHAN, F. A.; DERHAB, A. Formal analysis of language-based Android security using theorem proving approach. IEEE Access, v. 7, p. 16550-16560, 2019. DOI: https://doi.org/10.1109/ACCESS.2019.2895261.

HOFER-SCHMITZ, K.; STOJANOVIĆ, B. Towards formal verification of IoT protocols: a review. Computer Networks, v. 174, 107233, 2020. DOI: https://doi.org/10.1016/j.comnet.2020.107233.

LATIF, S.; REHMAN, A.; ZAFAR, N. A. NFA based formal modeling of smart parking system using TLA+. In: IEEE INTERNATIONAL CONFERENCE ON INFORMATION SCIENCE AND COMMUNICATION TECHNOLOGY (ICISCT), 2019, Karachi. Proceedings […]. Karachi: IEEE, 2019. DOI: https://doi.org/10.1109/CISCT.2019.8777445.

LECOMTE, T. Teaching and training in formalisation with B. In: DUBOIS, C.; SAN PIETRO, P. (Eds.). Formal Methods Teaching. FMTea 2023. Lecture Notes in Computer Science, v. 13962. Cham: Springer, 2023. DOI: https://doi.org/10.1007/978-3-031-27534-0_6.

LEVAC, D.; COLQUHOUN, H.; O’BRIEN, K. K. Scoping studies: advancing the methodology. Implementation Science, v. 5, p. 1-9, 2010. DOI: https://doi.org/10.1186/1748-5908-5-69.

LIU, Z.; LIU, J. Formal verification of blockchain smart contract based on colored petri net models. In: IEEE ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 43., 2019, Milwaukee. Proceedings […]. Milwaukee: IEEE, 2019. p. 555-560. DOI: https://doi.org/10.1109/COMPSAC.2019.10265.

LUKÁCS, G.; BARTHA, T. Conception of a formal model-based methodology to support railway engineers in the specification and verification of interlocking systems. In: IEEE INTERNATIONAL SYMPOSIUM ON APPLIED COMPUTATIONAL INTELLIGENCE AND INFORMATICS (SACI), 16., 2022, Timisoara. Proceedings […].Timisoara: IEEE, 2022, p. 283-288. DOI: https://doi.org/10.1109/SACI55618.2022.9919532.

PETERS, M. D. J.; GODFREY, C.; MCINERNEY, P.; MUNN, Z.; TRICCO, A. C.; KHALIL, H. Scoping reviews. In: AROMATARIS E, LOCKWOOD, C.; PORRITT, K.; PILLA, B.; JORDAN, Z. (Eds.). JBI Manual for Evidence Synthesis. JBI, 2024. DOI: https://doi.org/10.46658/JBIMES-24-09.

PRESSMAN, R. S.; MAXIM, B. R. Engenharia de software. 9. ed. Porto Alegre: McGraw Hill, 2021.

RAJABLI, N.; FLAMMINI, F.; NARDONE, R.; VITTORINI, V. Software verification and validation of safe autonomous cars: a systematic literature review. IEEE Access, v. 9, p. 4797-4819, 2021. DOI: https://doi.org/10.1109/ACCESS.2020.3048047.

RATIU, D.; GARIO, M.; SCHOENHAAR, H. FASTEN: an open extensible framework to experiment with formal specification approaches. In: IEEE/ACM INTERNATIONAL CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING (FORMALISE), 7., Montreal, 2019. Proceedings […]. 2019, p. 41-50. DOI: https://doi.org/10.1109/FormaliSE.2019.00013.

REZENDE, D. A. Engenharia de software e sistemas de informação. Rio de Janeiro: Brasport, 2006.

RIZVI, S. W. A.; KHAN, R. A.; ASTHANA, R. Improving software requirements through formal methods. International Journal of Information and Computation Technology, v. 3, n. 11, p. 1217-1223, 2013. Disponível em: https://www.ripublication.com/irph/ijict_spl/13_ijictv3n11spl.pdf. Acesso em: 12 ago. 2024.

ROGGENBACH, M.; CERONE, A.; SCHLINGLOFF, B.-H.; SCHNEIDER, G.; SHAIKH, S. A. Formal methods for software Engineering: languages, methods, applications domains. Springer, 2021. DOI: https://doi.org/10.1007/978-3-030-38800-3.

ROULAND, Q.; HAMID, B.; BODEVEIX, J.-P.; FILALI, M. A formal methods approach to security requirements specification and verification. In: 2019 INTERNATIONAL CONFERENCE ON ENGINEERING OF COMPLEX COMPUTER SYSTEMS (ICECCS), 24., 2019, Guangzhou. Proceedings […]. Guangzhou: IEEE, 2019. p. 236-241. DOI: https://doi.org/10.1109/ICECCS.2019.00033.

SCAICO, A. Aplicação de métodos formais no projeto de interfaces para sistemas industriais críticos. Dissertação (Mestrado em Engenharia Elétrica) – Universidade Federal de Campina Grande, Campina Grande, 2007. Disponível em: http://dspace.sti.ufcg.edu.br:8080/jspui/handle/riufcg/6270. Acesso em: 13 ago. 2024.

SHIGYO, Y.; KATAYAMA, T. Proposal of an approach to generate vdm++ specifications from natural language specification by machine learning. In: IEEE Global Conference on Consumer Electronics (GCCE), 9., 2020, Kobe. Proceedings […]. Kobe: IEEE, 2020, p. 292-296. DOI: https://doi.org/10.1109/GCCE50665.2020.9292047.

SIREGAR, M. U.; ABRIANI, S. Verification of a rule-based expert system by using SAL model checker. In: IEEE International Conference on Informatics and Computational Sciences (ICICoS), 3., 2019, Semarang. Proceedings […]. Semarang: IEEE, 2019. DOI: https://doi.org/10.1109/ICICoS48119.2019.8982426.

SOMMERVILLE, I. Engenharia de software. 10. ed. São Paulo: Pearson, 2019.

WESTPHAL, B. On complementing an undergraduate software engineering course with formal methods. In: IEEE CONFERENCE ON SOFTWARE ENGINEERING EDUCATION AND TRAINING (CSEE&T), 32., 2020, Munich. Proceedings […]. Munich: IEEE, 2020, p. 1-10. DOI: https://doi.org/10.1109/CSEET49119.2020.9206234.

YOUNES, A. B.; HLAOUI, Y. B. D.; AYED, L. B.; BESSIFI, M. From BPMN2 to event B: a specification and verification approach of workflow applications. In: IEEE ANNUAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE (COMPSAC), 43., 2019, Milwaukee. Proceedings […]. Milwaukee: IEEE, 2019, p. 561-566. DOI: https://doi.org/10.1109/COMPSAC.2019.10266.

XAVIER, A.; MARTINS, F.; PIMENTEL, R.; CARVALHO, D. Aplicação da UML no contexto das metodologias ágeis. In: ENCONTRO NACIONAL DE COMPUTAÇÃO DOS INSTITUTOS FEDERAIS, 6., 2019, Belém. Anais [...]. Belém: SBC. DOI: https://doi.org/10.5753/encompif.2019.6353.

ZHAO, H.; ZHU, H.; FANG, Y.; XIAO, L. Modeling and verifying storm using CSP. In: IEEE INTERNATIONAL SYMPOSIUM ON HIGH ASSURANCE SYSTEMS ENGINEERING (HASE), 19., 2019, Hangzhou. Proceedings […].Hangzhou: IEEE, 2019. p. 192-199. DOI: https://doi.org/10.1109/HASE.2019.00037.

ZHANG, W.; SALCIC, Z.; MALIK, A. Towards formal modeling and analysis of SystemJ GALS systems using coloured petri nets. In: IEEE INTERNATIONAL CONFERENCE ON INDUSTRIAL INFORMATICS (INDIN), 17., 2019, Helsinki. Proceedings […]. Helsinki: IEEE, 2019, p. 152-159. DOI: https://doi.org/10.1109/INDIN41052.2019.8972025.

ZHU, J.; HU, K.; FILALI, M.; BODEVEIX, J.-P.; TALPIN, J.-P.; CAO, H. formal simulation and verification of solidity contracts in event-B. In: 2021 IEEE ANNUAL COMPUTERS, SOFTWARE, AND APPLICATIONS CONFERENCE (COMPSAC), 45., 2021, Madrid. Proceedings […]. Madrid: IEEE, 2021. p. 1309-1314. DOI: https://doi.org/10.1109/COMPSAC51774.2021.00183.


DOI: http://dx.doi.org/10.18265/2447-9187a2024id8404

O arquivo PDF selecionado deve ser carregado no navegador caso tenha instalado um plugin de leitura de arquivos PDF (por exemplo, uma versão atual do Adobe Acrobat Reader).

Como alternativa, pode-se baixar o arquivo PDF para o computador, de onde poderá abrí-lo com o leitor PDF de sua preferência. Para baixar o PDF, clique no link abaixo.

Caso deseje mais informações sobre como imprimir, salvar e trabalhar com PDFs, a Highwire Press oferece uma página de Perguntas Frequentes sobre PDFs bastante útil.

Download do PDF
Imprimir artigo
Exibir metadados
Como citar este documento

Visitas a este artigo: 258

Total de downloads do artigo: 174