DReason - Técnicas Dedutivas para a Verificação de Sistemas Distribuídos e Protocolos | Referência: 2024.15569.PEX

A fiabilidade de software deve ser mais que uma mera possibilidade ou promessa teórica. Se vivemos num mundo que, literalmente, funciona sobre software é fundamental podermos confiar nas infraestruturas computacionais das quais dependemos. Se a nossa ambição é produzir programas confiáveis, devemos ser capazes de trazer as garantias do raciocínio matemático para o ciclo de desenvolvimento de software. Este é exatamente o propósito da verificação formal. Podemos citar diferentes abordagens e técnicas: verificação de modelos, análises estáticas, verificação dedutiva ou teorias de tipos expressivas. Todas estas técnicas têm um objetivo comum: aumentar a confiança sobre software que se coloca em execução. Em particular, software que corre numa escala global e que cumpre tarefas exigentes. Acreditamos que sistemas distribuídos, dada a sua adoção e implementação massivas, devem tornar-se alvos reais da verificação formal.
A verificação de sistemas distribuídos e protocolos é um desafio importante. Tem sido abordado através de diferentes metodologias, desde verificação de modelos até à verificação dedutiva usando ferramentas interactivas. Estas últimas sofrem de um inconveniente óbvio: mesmo que possam assegurar garantias fortes sobre o código, provas interativas dificilmente se tornarão  a escolha de peritos em sistemas distribuídos. Se queremos trazer a verificação dedutiva para o domínio da computação distribuída, devemos ter um foco claro na automação. Frequentemente consideradas como limitadas e pouco expressivas, ferramentas automáticas de verificação dedutiva são atualmente alvo de investigação intensiva e conheceram avanços tremendos nos últimos anos, ao ponto de serem utilizados na verificação de software complexo. No entanto, se ambicionamos a adopção de técnicas de verificação por engenheiros de sistemas distribuídos, que não são necessariamente peritos em provas de programas, devemos também desenvolver linguagens e ferramentas que permitam uma definição abstracta e simulações simples de protocolos e sistemas distribuídos. Assim, plataformas de verificação devem traduzir estas descrições de alto nível de protocolos para linguagens orientadas à prova.
Neste projeto utilizaremos a linguagem Lupin como alicerce para a construção de uma plataforma que permita especificar, verificar automaticamente e executar protocolos distribuídos. Lupin é atualmente capaz de descrever protocolos de consenso simples, pretendemos por isso estender a expressividade da linguagem para suportar uma classe maior de sistemas distribuídos. Utilizaremos a plataforma Why3 como meio de raciocínio para construir uma ferramenta de verificação automática de sistemas distribuídos. Esta ferramenta será baseada na biblioteca Why3-do que apresenta um conjunto de definições formais de modelos de sistemas distribuídos e redes, formalizados com recurso à linguagem lógica e de programação do Why3.
A nossa equipa reúne investigadores com experiência em verificação e linguagens de programação. O IR é membro da equipa de desenvolvimento do Why3 e tem larga experiência no desenho de linguagens de especificação e ferramentas para a verificação de programas funcionais. É também membro da equipa o principal arquitecto da biblioteca Why3-do. Finalmente, os outros dois membros core são os criadores da linguagem Lupin e ambiente de simulação associado. Acreditamos que a equipa apresenta a combinação perfeita de capacidades e conhecimento para conduzir com sucesso este projeto e produzir resultados científicos de grande relevo. O principal resultado esperado deste projeto será uma plataforma completa para de especificação e verificação, indo de código Lupin anotado até implementações corretas e executáveis de protocolos.
Período de execução: 1 de fevereiro de 2026 a 31 de julho de 2027.