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

Autores

DOI:

https://doi.org/10.18265/2447-9187a2024id8404

Palavras-chave:

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

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.

Downloads

Não há dados estatísticos.

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.

Downloads

Como Citar

MARQUES, C. A. N.; SILVA, M. A. F. da; ANDRADE, J. L. S. de; MILANEZ, A. F. Linguagens e ferramentas utilizadas na especificação formal de software: uma revisão de escopo. Revista Principia, [S. l.], v. 62, 2025. DOI: 10.18265/2447-9187a2024id8404. Disponível em: https://periodicos.ifpb.edu.br/index.php/principia/article/view/8404. Acesso em: 5 fev. 2025.

Edição

v. 62 (2025)

Seção

Ciência da Computação

Licença

Esta revista, seguindo as recomendações do movimento de Acesso Aberto, proporciona seu conteúdo em Full Open Access. Assim os autores conservam todos seus direitos permitindo que a Revista Principia possa publicar seus artigos e disponibilizar pra toda a comunidade.

A Revista Principia adota a licença Creative Commons 4.0 do tipo atribuição (CC-BY). Esta licença permite que outros distribuam, remixem, adaptem e criem a partir do seu trabalho, inclusive para fins comerciais, desde que lhe atribuam o devido crédito pela criação original.

Os autores estão autorizados a enviar a versão do artigo publicado nesta revista em repositório institucionais, com reconhecimento de autoria e publicação inicial na Revista Principia.

Demais informações sobre a Política de Direitos Autorais da Revista Principia encontram-se neste link. 

Artigos mais lidos pelo mesmo(s) autor(es)