Os investigadores Alcino Cunha (Haslab-EEUM) e Nuno Macedo (INESC TEC) contribuíram para o desenvolvimento do Alloy 6, a versão mais recente de uma das plataformas de especificação e análise mais utilizadas para a análise formal de designs nas fases iniciais do desenvolvimento de software.

Esta nova versão da linguagem apresenta novas primitivas que permitem especificar, validar e verificar modelos comportamentais de forma nativa. As técnicas de análise associadas ao Alloy foram também estendidas para suportar este tipo de análise, assim como o visualizador que apresenta instâncias durante a validação.

O Alloy, inicialmente desenvolvido pelo MIT, pode ser utilizado para modelar e analisar todos os tipos de sistemas, mas é principalmente útil em sistemas com propriedades estruturais complexas, tais como protocolos distribuídos ou sistemas com arquiteturas altamente configuráveis. Sendo baseado numa lógica simples, expressiva e baseada na noção de relações, e sendo apoiado por análises formais automáticas, o Alloy é bastante útil para rapidamente explorar diferentes opções de design, bem como para verificar se o comportamento esperado é garantido.

A vantagem do Alloy 6 é que permite combinar esta análise estrutural com análise comportamental, o que até agora precisava de ser codificado manualmente. Esta extensão preserva também a simplicidade e flexibilidade características do Alloy, tornando o Alloy 6 a plataforma ideal para a análise do design de sistemas ricos em propriedades estruturais e comportamentais.

Os investigadores do Laboratório de Software Confiável (HASLab), em conjunto com uma equipa de investigadores do ONERA (Laboratório Aeroespacial Francês), desenvolveram esta extensão ao Alloy como uma ferramenta independente, o Electrum, no contexto do projeto de investigação TRUST. Ainda assim, após o reconhecimento da comunidade científica, esta extensão foi integrada na distribuição oficial do Alloy.

Os investigadores da EEUM e INESC TEC mencionados na notícia têm vínculo à UMinho e UP-FEUP.