Egresso do IMD valida tecnologia de métodos formais com empresa francesa

Em estágio de seis meses na ClearSy, doutorando da UFRN desenvolve ferramenta para sistemas críticos
Felipe Araújo

Um egresso do Instituto Metrópole Digital (IMD/UFRN) e doutorando do Departamento de Informática e Matemática Aplicada (DIMAp), ultrapassou as barreiras geográficas do conhecimento científico após, nos últimos seis meses, desenvolver e integrar uma tecnologia inédita junto à ClearSy – empresa francesa especializada em engenharia de sistemas críticos e no desenvolvimento de soluções baseadas em métodos formais.

Entre março e setembro deste ano, o estudante Fagner Dias esteve na sede da empresa, em Aix-en-Provence, no sul da França, para aprimorar uma solução voltada à verificação de códigos utilizados em sistemas críticos – como aqueles utilizados em automações de trens e metrôs.

O trabalho de Dias consiste em um plugin para uma ferramenta da ClearSy que permite verificar, matematicamente, especificações de sistemas e gerar códigos executáveis, acrescentando uma etapa de verificação do próprio código produzido para ampliar a segurança do processo e o uso desse tipo de tecnologia, amplamente utilizada em países europeus, uma das maiores concentrações de linhas ferroviárias do mundo.

Para o estudante, a experiência do estágio foi importante tanto para sua formação acadêmica quanto para sua trajetória profissional.

“Ter o contato in loco de pessoas trabalhando com a área, não somente no laboratório, não somente em pesquisas e lendo artigos, faz uma grande diferença. É importante saber o que está sendo utilizado hoje em dia no mercado e em quais áreas, como linhas ferroviárias, sistemas de trem e usinas nucleares. Foi muito importante, até para talvez, depois do meu doutorado, tentar um pós-doc lá na França”, comenta Dias.

Pesquisa

Na prática, o novo recurso produzido na pesquisa de Fagner Dias acrescenta uma nova etapa a esse processo de segurança: verificar se o código gerado realmente corresponde ao que foi especificado.

Em outras palavras, em um sistema de automação de trens, por exemplo, seria possível verificar se comandos como controle de velocidade ou abertura e fechamento de portas estão de acordo com as regras definidas para o funcionamento do sistema.

O trabalho integra a pesquisa de doutorado de Dias, desenvolvida na área de métodos formais. Antes disso, o estudante já foi matriculado na primeira turma do Bacharelado em Tecnologia da Informação (BTI/IMD), ele posteriormente cursou Engenharia de Computação e fez mestrado no DIMAp, onde também curso seu doutorado. Além disso, Dias também participou do programa de Residência em TI junto ao Tribunal de Justiça do Estado (TJRN).

A próxima etapa da pesquisa será validar o próprio plugin, por meio da construção das regras que permitam comprovar matematicamente que ele realiza corretamente a função para a qual foi desenvolvido.

Fagner prevê concluir o doutorado no início de 2028 e pretende continuar atuando na área de métodos formais. A experiência internacional também ampliou seu interesse por oportunidades profissionais fora do Brasil, inclusive com a possibilidade de realizar um pós-doutorado na França.

ClearSy

A aproximação entre a UFRN e a ClearSy também tem sido fortalecida por iniciativas promovidas pelo IMD. A parceria entre a universidade e a empresa existe desde 2016 e, em julho deste ano, resultou na terceira edição do hackathon de Métodos Formais na Engenharia de Software.

“A parceria entre a UFRN e a ClearSy tem proporcionado aos alunos do DIMAp e do IMD uma oportunidade diferenciada de formação internacional, permitindo que eles apliquem, em um ambiente industrial, os conhecimentos em Métodos Formais adquiridos na Universidade. Essa experiência possibilita aos estudantes trabalhar com problemas e tecnologias reais, consolidar sua formação e vivenciar a aplicação prática de uma área na qual a UFRN possui reconhecida competência acadêmica”, explica Marcel.