Qual é a sua experiência com verificação de modelo de software?[fechado]

Question

• Que tipos de aplicativos você usou verificação de modelo para?
• Qual ferramenta de verificação de modelo você usou?
• Como você resumiria sua experiência com a técnica, especificamente na avaliação de sua eficácia no fornecimento de software de maior qualidade?

Durante meus estudos, tive a oportunidade de usar Rodar, e isso despertou minha curiosidade sobre a quantidade real de verificação de modelos e quanto valor as organizações estão obtendo com isso.Na minha experiência profissional, trabalhei em aplicações de negócios, onde (naturalmente) não há consideração de aplicação de verificação formal à lógica.Eu realmente gostaria de aprender sobre o modelo do pessoal do SO, verificando experiências e pensamentos sobre o assunto.A verificação de modelo algum dia se tornará uma prática de desenvolvimento mais amplamente utilizada que deveríamos ter em nosso kit de ferramentas?

Answer 1

Acabei de terminar uma aula sobre verificação de modelos e as grandes ferramentas que usamos foram Rodar e SMV.Acabamos usando-os para verificar propriedades de problemas comuns de sincronização e achei o SMV um pouco mais fácil de usar.

Embora essas ferramentas sejam divertidas de usar, acho que elas realmente brilham quando você as combina com algo que impõe restrições dinamicamente ao seu programa (para que seja um pouco mais fácil verificar coisas "úteis" sobre o seu programa).Acabamos pegando o Estrutura Spring WebFlow, que usa XML para escrever um arquivo semelhante a uma máquina de estado que especifica quais páginas da web podem fazer a transição para quais outras, e usa SMV para poder realizar a verificação em tais aplicativos (plug sem vergonha aqui).

Para responder à sua última pergunta, acho que a verificação de modelo é definitivamente útil, mas me inclino mais a usar testes de unidade como uma técnica que me faz sentir confortável ao entregar meu produto final.

Answer 2

Usamos vários verificadores de modelos no ensino, no projeto e no desenvolvimento de sistemas.Nossa caixa de ferramentas inclui SPIN, UPPAL, Java Pathfinder, PVS e Bogor.Cada um tem seus pontos fortes e fracos.Todos encontram problemas com modelos que são simplesmente impossíveis de serem descobertos pelos seres humanos.Sua usabilidade varia, embora a maioria seja automatizada por botão.

Quando usar um verificador de modelo?Eu diria que sempre que você estiver descrevendo um modelo que deve ter (ou não) propriedades específicas e é maior do que um punhado de conceitos.Quem pensa que pode descrever e compreender algo maior ou mais complexo está se enganando.

Answer 3

Para quais tipos de aplicativos você usou a verificação de modelo?

Usamos o verificador de modelo Java Path Finder para verificar algumas propriedades de segurança (deadlock, condição de corrida) e temporais (usando lógica temporal linear para especificá-las).Ele suporta asserções clássicas (como NotNull) em Java (bytecode) - é para verificação de modelo de programa.

Qual ferramenta de verificação de modelo você usou?

Nós costumavamos Localizador de caminho Java (para fins acadêmicos).É um software de código aberto desenvolvido inicialmente pela NASA.

Como você resumiria sua experiência com a técnica, especificamente na avaliação de sua eficácia no fornecimento de software de maior qualidade?

A verificação do modelo do programa tem um grande problema com a explosão do espaço de estados (uso de memória e disco).Mas existe uma grande variedade de técnicas para reduzir os problemas, para lidar com grandes artefatos, como redução parcial de ordem, abstração, redução de simetria, etc.

Answer 4

Usei o SPIN para encontrar um problema de simultaneidade no software PLC.Ele encontrou uma condição de corrida insuspeitada que teria sido muito difícil de encontrar por meio de inspeção ou teste.

A propósito, existe um livro "SPIN for Dummies"?Tive que aprender no livro "The SPIN Model Checker" e em vários tutoriais on-line.

Answer 5

Fiz algumas pesquisas sobre esse assunto durante meu período na universidade, ampliando o Verificador de modelo de montagem de exploração de estado.

Utilizamos uma máquina virtual para percorrer todos os caminhos/estados possíveis do programa, usando A* e alguma heurística, dependendo do tipo de erro (deadlock, erros de I/O, ...)

Foi inspirado em Desbravador Java e funcionou com código C++.(Tudo o que o GCC poderia compilar)

Mas, em nossas experiências, esse tipo de tecnologia não será usada em aplicações de negócios em breve, devido a problemas relacionados à GUI, ao trabalho necessário para criar um ambiente de teste inicial e aos enormes requisitos de hardware.(Você precisa de muita RAM e espaço em disco, devido ao gigantesco espaço de estado)