Linguagens e ferramentas utilizadas na especificação formal de software: uma revisão de escopo
DOI:
https://doi.org/10.18265/2447-9187a2024id8404Palavras-chave:
especificação de software, métodos formais, modelagem formal, validação de software, verificação formalResumo
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
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.
Edição
Seção
Licença
• O(s) autor(es) autoriza(m) a publicação do artigo na revista;
• O(s) autor(es) garante(m) que a contribuição é original e inédita e que não está em processo de avaliação em outra(s) revista(s), nem esteja publicado em anais de congressos e/ou portais institucionais;
• A revista não se responsabiliza pelas opiniões, ideias e conceitos emitidos nos textos, por serem de inteira responsabilidade de seu(s) autor(es). Opiniões e perspectivas expressas no texto, assim como a precisão e a procedência das citações, são de responsabilidade exclusiva do(s) autor(es), e contribuem para a promoção dos:
- Princípios FAIR (Findable, Accessible, Interoperable, and Reusable – localizável, acessível, interoperável e reutilizável);
- Princípios DEIA (diversidade, equidade, inclusão e acessibilidade).
• É reservado aos editores o direito de proceder ajustes textuais e de adequação do artigos às normas da publicação.
Responsabilidades dos autores e transferência de direitos autorais
Os autores devem declarar a originalidade do estudo, bem como o fato de que este não foi publicado anteriormente ou está sendo considerado para publicação em outro meio, como periódicos, anais de eventos ou livros. Ao autorizarem a publicação do artigo na Revista Principia, os autores devem também responsabilizar-se pelo conteúdo do manuscrito, cujos direitos autorais, em caso de aprovação, passarão a ser propriedade exclusiva da revista. A Declaração de Responsabilidades dos Autores e Transferência de Direitos Autorais deverá ser assinada por todos os autores e anexada ao sistema como documento suplementar durante o processo de submissão. Clique no link abaixo para fazer o download do modelo.
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.
