A Univesidade Federal do Rio Grande do Norte (UFRN) e a empresa francesa ClearSy irão apresentar seu mais recente trabalho conjunto sobre a verificação formal de código C gerado a partir de modelos B na Conferência Internacional SBMF 2025. O evento, também conhecido como Simpósio de Métodos Formais, será realizado em Recife, Brasil, entre os dias 2 e 5 de dezembro.

O artigo, intitulado "Brigding the B-Method and ACSL: Towards Verified C Code", foi desenvolvido por um aluno do Programa de Pós-graduação em Sistemas e Computação (PPgSC/UFRN), orientado pelo professor Marcel Oliveira, do Departamento de Informática e Matemática Aplicada (Dimap/UFRN) e do pesquisador da Clearsy Thierry Lecomte. Todo o desenvolvimento do projeto ocorreu no Laboratório ForAll, do Núcleo Integrador de Pesquisa e Inovação em Engenharia de Software (SETE/IMD).

Segundo Oliveira, essa é a terceira vez que um trabalho feito pela UFRN junto à empresa francesa é apresentado no Simpósio.

“Esse é um resultado de uma parceria entre a Universidade e a ClearSy, a qual é de grande importância por unir excelência acadêmica com a experiência prática e industrial dessa empresa francesa. Isso amplia a visibilidade internacional da UFRN e contribui para a adoção de soluções mais seguras e confiáveis em setores estratégicos como transporte, automação e software embarcado”, comenta Marcel Oliveira

A pesquisa

O estudo pesquisou uma questão crucial para a indústria de sistemas de segurança: como fortalecer a confiança em softwares gerados automaticamente.

Isso ocorre porque o Método B é um método formal de desenvolvimento de software que utiliza técnicas de especificação e verificação para garantir que um sistema funcione conforme o planejado, ainda na fase de modelagem. Exemplo disso é o de um engenheiro que pode provar que um elevador nunca abrirá as portas enquanto estiver em movimento.

No entanto, garantir que o código C gerado automaticamente a partir desses modelos continue obedecendo a essas mesmas propriedades — ou seja, que o programa final realmente siga as regras comprovadas no modelo — ainda é um desafio importante.

Para enfrentar essa questão e garantir essa segurança, os autores da pesquisa propõem a geração sistemática de asserções ACSL — linguagem de especificação usada para descrever o comportamento esperado de programas escritos em C — a partir de modelos B.

Essas asserções são processadas pelo Frama-C, uma ferramenta de análise estática que permite verificar formalmente se o código C atende aos requisitos definidos nos modelos matemáticos originais.

Essa proposta possibilita aos engenheiros confirmem, de forma automatizada e precisa, que sistemas embarcados críticos — como os usados em trens, aviões ou equipamentos médicos — se comportam exatamente conforme projetado. Na prática, isso reduz o risco de falhas em operação, aumenta a confiabilidade do software e agiliza o processo de certificação de sistemas de segurança.

“A pesquisa fomenta o desenvolvimento de novas técnicas e ferramentas de verificação, promove a formação de recursos humanos altamente qualificados, estimula publicações e projetos conjuntos, e impulsiona a transferência de tecnologia entre academia e indústria”, comenta Marcel Oliveira.

Segundo a ClearSy, ao combinar o rigor matemático com ferramentas modernas de verificação, a empresa continua a aproximar a engenharia de segurança ferroviária das tecnologias de software atuais, demonstrando que o futuro do transporte ferroviário depende da lógica formal e da inovação.

ClearSy

A colaboração entre o IMD e a ClearSy tem sido prolífica, resultando em pesquisas conjuntas, publicações científicas e ações de formação internacional. Um dos frutos dessa parceria é a criação de um MOOC (Massive Open Online Course) sobre o Método B, voltado à disseminação de práticas formais de engenharia de software.

Recentemente, a ClearSy patrocinou a 3ª edição de um hackathon no IMD, realizado ao longo do mês de julho, que desafiou os participantes a criar um software capaz de estimar a ocupação de trilhos – funcionalidade essencial para evitar colisões entre veículos ferroviários e otimizar o fluxo em malhas urbanas e intermunicipais.

A parceria internacional também já gerou oportunidades diretas de carreira para estudantes da UFRN, como um acordo de cooperação entre a universidade e a ClearSy, intermediado pelo IMD, que regulamenta a realização de estágios na sede da empresa, na França. A oportunidade oferece cobertura completa das despesas da viagem, moradia, seguro-saúde, auxílio-refeição e transporte, sendo todos esses custos arcados pela ClearSy.