Os métodos formais não são apenas para desenvolver software crítico. Um investigador INESC TEC explicou porquê numa conferência internacional

Ao longo de dois dias, a comunidade de programação funcional reuniu-se no maior evento da área no sul da Europa, estabelecendo pontes entre o que de melhor se faz na academia e a aplicação no mundo industrial.  

Alcino Cunha, investigador do INESC TEC, foi um dos oradores convidados do Lamba World, uma conferência internacional na área da programação funcional e respetivas aplicações. Enquanto palco privilegiado para o encontro de múltiplas linguagens de programação, o evento permitiu também o contacto entre académicos, representantes da indústria e entusiastas da área. 

Na sua palestra, intitulada Designing Software with Complex Configurations, Alcino Cunha focou-se no desenho de software com configurações complexas usando métodos formais “leves”, com destaque para as linguagens TLA+ e Alloy. O objetivo foi demonstrar a aplicação das mesmas na especificação e verificação de um protocolo distribuído simples e que é expectável que funcione em diferentes configurações de rede. 

Os métodos formais são uma técnica matemática poderosa na conceção de software. No entanto, muitos destes métodos tem uma elevada dificuldade e custo inerentes à sua utilização. A alternativa surge por via dos métodos formais “leves”, uma alternativa que enfatiza o uso de ferramentas de análise automática para detetar problemas em  especificações parciais do sistema a desenvolver. 

É precisamente neste grupo que podem ser encontradas as linguagens Alloy e TLA+, linguagens cuja aplicação é especialmente útil na rápida exploração de diferentes opções de design, mas também para garantir que o comportamento do software satisfaz os requisitos esperados.  

Num workshop intitulado Structural Design with Alloy, o investigador do INESC TEC abordou também o uso deste método formal “leve” para a conceção de estruturas de software. Partindo do mote da linguagem Alloy — “tudo é uma relação” — os participantes tiveram a oportunidade de aprender a modelar estruturas por via de um simples conceito matemático, como especificar os requisitos das referidas estruturas através da lógica relacional da Alloy. Finalmente, foi explicado de que forma estes modelos formais poderão ser utilizados para automatizar o processo de teste da implementação de estruturas de dados.  

Perante a índole mais industrial da conferência, Alcino Cunha destaca o “entusiasmo” com que a sua talk foi recebida, destacando também os contactos que foram feitos logo de seguida com vista à implementação das ideias partilhadas. “É um bocadinho diferente das conferências em que costumo participar, onde se costuma discutir apenas questões técnicas. Neste caso, os assuntos foram abordados do ponto de vista do utilizador”. Esta interação tornou a partilha, nas palavras do próprio, mais “gratificante”. “É uma forma excelente de chegarmos à indústria”, concluiu.  

O investigador do INESC TEC mencionado na notícia tem vínculo ao INESC TEC e à UMinho. 

  

PHP Code Snippets Powered By : XYZScripts.com
EnglishPortugal