Programa de Verificação Formal crowdsourced Gera Milhares de informações para Softwares


A fase inicial de um programa DARPA que usou jogos online acessíveis ao público para acelerar a verificação de software ajudou a produzir centenas de milhares de anotações de programas em linguagens de programação de software comum, acrescentando credibilidade à ideia de que os jogos digitais podem ser um meio eficaz de soluções de crowdsourcing para problemas de software. Os resultados têm inspirado DARPA para lançar uma nova rodada de jogos com o objetivo de estender os êxitos até à data e aprender mais sobre o potencial da abordagem.

"Estamos animados com esses resultados e estão incentivando o público a utilizar os nossos jogos novos ao longo das próximas semanas para que possamos ver o quão longe esta abordagem pode ir", disse Michael Hsieh, gerente do programa DARPA. "O crescimento de sistemas de software na década passada superou melhorias na verificação. Há especialistas simplesmente não suficientes para fornecer análise manual na escala necessária para suportar a verificação formal dos sistemas de software incontáveis ​​lançados a cada dia."

Software não confiável impõe custos significativos sobre os EUA e as economias globais. Práticas de desenvolvimento existentes resultam em software que contém cerca de 1-5 bugs ou erros por cada mil linhas de código. Verificação programa formal - abordagem matemática para assegurar a precisão fundamental de código - é a melhor maneira de ter certeza de que uma determinada peça de software é livre de certos tipos de erros. Mas verificação formal hoje é quase sempre feito manualmente por engenheiros especialmente treinados, e é muito caro para ser aplicado depois de componentes de software, pequenas críticas.

Em dezembro de 2013, o programa da DARPA Multidão Originário Formal Verification (CSFV) lançou a primeira versão do portal web Verigames ( www.verigames.com ), que oferecia cinco jogos de verificação formal online grátis. Estes jogos traduzidos ações dos jogadores em anotações do programa e assistida especialistas de verificação formal na geração de provas matemáticas para verificar a ausência de importantes classes de falhas no software escritas na "C" e linguagens de programação "Java". Uma análise inicial indica que os não-especialistas que jogam jogos de CSFV gerado centenas de milhares de anotações.

Para saber mais sobre o potencial desta abordagem para verificação crowdsourcing, CSFV lançou recentemente cinco novos jogos no www.verigames.com , projetado para melhor jogabilidade, bem como uma maior eficácia de verificação do software:

Dynamakr: Solicita jogadores para energizar padrões misteriosos em uma máquina quebra-cabeça cósmico
Paradoxo: Solicita jogadores a usar um conjunto de ferramentas para otimizar vastas redes
Santo Mapa Hyperspace: Solicita jogadores para a batalha invasores alienígenas e selar fora de suas fendas hiperespaço
Monstro prova: Solicita aos jogadores explorar um reino de monstros e resolver quebra-cabeças para ficar rico
Fissão binária: Um jogo átomo-splitting que pede que os jogadores de misturar e combinar quarks em nome da segurança cibernética

Jogos CSFV estão abertos apenas para jogadores idades acima de 18 anos.

Fonte: http://www.darpa.mil

Comentários