Experiências com o uso de liga em projetos do mundo real

Question

Estou interessado em métodos formais há algum tempo. Usei métodos formais para raciocinar sobre algumas subáreas muito específicas de alguns projetos em que tenho trabalhado. Nunca fui capaz de convencer outros membros da equipe a tentar o mesmo especificar um domínio inteiro com um método formal.

Um método que achei particularmente interessante é Liga. Eu acho que pode "escalar" melhor como base para um projeto inteiro, porque é conceitualmente e noticamente muito próximo das linguagens de programação reais. Além disso, as ferramentas são bastante sólidas para que os benefícios da verificação do modelo estejam prontamente disponíveis.

Eu ficaria muito interessado em ouvir sobre quaisquer experiências do mundo real que vocês tenham tido com o uso de liga em seus projetos. Você acha que isso o ajudou a projetar um modelo de domínio melhor? Encontrou erros no seu modelo de domínio durante a verificação? Você usaria de novo?

Answer 1

Sim, eu usei liga e são primos industrialmente. A liga tem sido mais útil para me convencer de que meus modelos não estavam extremamente errados-ou melhor, me mostrando onde estavam errados e deram origem a resultados tolos. Outras ferramentas mais específicas, como Athena e Guttman e Ramsdell, da Song, foram mais úteis em seus domínios mais estreitos. O que mais você gostaria de ouvir?

Answer 2

Eu usei liga em alguns projetos e achei útil; Em alguns, mas não em todos esses projetos, pude convencer outros envolvidos a usar liga também, ou pelo menos trabalhar com os modelos de liga que escrevi. Esses projetos podem ou não ser o que você tem em mente ao pedir projetos do 'mundo real', mas eles certamente ocorreram na parte do mundo real em que trabalho.

Em 2006 e 2007, criei um modelo de liga parcial para o rascunho da corrente da especificação W3C XPROC; Até onde eu sabia, a maioria dos membros do grupo de trabalho nunca leu o artigo que escrevi (em http://www.w3.org/xml/xproc/2006/12/alloy-models/models.html); Eles disseram "Oh, mudamos essa parte da especificação na semana passada, então o que o modelo diz não é mais relevante". Mas o artigo conseguiu convencer o editor da especificação de que o nível de 'componente' abstrato descrito no primeiro rascunho das especificações era lamentavelmente indispecificado e precisava ser totalmente especificado ou descartado. Ele o abandonou, com (eu acho) bons resultados para a legibilidade e usabilidade das especificações.

Em 2010 eu fiz um Modelo de liga do modelo de dados XPath 1.0, que descobriu algumas falhas na especificação. A reação das partes mais interessadas (incluindo o Grupo de Trabalho do W3C responsável por manter a especificação XPath 1.0), infelizmente, não foi encorajadora.

Um projeto de pesquisa com o qual estou envolvido usou liga para modelar o corpus do MLCD, uma coleção de documentos de amostra e informações relacionadas que estamos criando (hiperlinks suprimidos na insistência de So); O modelo de liga encontrou alguns erros em nosso design inicial para o catálogo corpus, por isso valeu a pena o esforço.

E também usamos liga para formalizar algum trabalho de modelagem que fizemos sobre a natureza da transcrição e a extensão da distinção do tipo/token para documentar a estrutura (para o nosso artigo, procure os procedimentos de 2010 da Balisage: a Conferência de Markup). Isso está um pouco fora da área de aplicação usual da liga, pois não tem nada a ver com o design de software, mas a capacidade de Alloy de verificar os modelos de consistência e gerar instâncias tem sido inestimável para nos mostrar algumas das consequências lógicas deste ou do possível axioma para o nosso modelo.

Para responder às suas perguntas específicas: Sim, a liga me ajudou a especificar modelos de domínio mais limpos e, sim, encontrou erros e falhas. Eles costumam ser pequenos, pelos motivos pelos quais Daniel Jackson explica em seu livro Abstrações de software: Primeiro, se você usa modelos durante o design, assumirá erros mais cedo, quando tudo ainda é pequeno. E, segundo (nas palavras de Jackson), "em retrospectiva, a maioria dos problemas de design de software é trivial".

Ele continua: "Mas se você não os aborda de frente, os problemas triviais têm o hábito desagradável de se tornarem não triviais". Minha experiência confirma amplamente isso. Muito melhor para afastar esses problemas mais cedo. Então, sim, vou usar a liga novamente.

Answer 3

Adicionando tardiamente a este tópico ... Eunsuk Kang aplicou recentemente liga para realizar análises de segurança de APIs da Web para algumas start -ups (seguindo muitas aplicações de liga em segurança, como o Apurva's Análise de Oauth e Barth et al Análise de mecanismos de segurança baseados no navegador para CSRF etc); Pamela Zave tem trabalhado em um Análise impressionante do acorde, um sistema de armazenamento pares para pares e recentemente escreveu uma correção para o algoritmo original.