A nossa abordagem, parte deste facto pouco animador, para dois pressupostos: havendo a consciência desta impraticabilidade, sabe-se, que a tarefa de analisar e provar matematicamente a correcção e a coerência de um conjunto de requisitos, devidamente formalizados, é perfeitamente realizável. Mais ainda, há evidências científicas de que a esmagadora maioria dos problemas graves em sistemas se devem ao insuficiente tratamento de requisitos (e.g. pela existência de incoerências, ambiguidades, etc). Por razão maior, temos que o uso da prova, ao nível do tratamento de requisitos, evita os mencionados problemas; a aplicação de testes é, portanto, a via operacional para a validação do produto final. As limitações inerentes às metodologias de validação por testes são sobejamente conhecidas: para além da impossibilidade de cobrir todo o domínio de teste de um sistema, há a problemática da adequação dos testes aos requisitos. I.e., não é por vezes claro que um teste esteja bem implementado em relação ao requisito que se pretende validar com a sua aplicação. Sugere-se neste projecto que os testes sejam directamente gerados a partir da especificação formal de requisitos, havendo assim a garantia matemática da sua adequação. Mais ainda, esta geração é feita de forma automática, o que representa um aspecto muito significativo, dado o volume despendido de esforço na fase de teste do desenvolvimento de um produto.

Assim, contrariando o dogma da incompatibilidade entre testes e provas, acreditamos ser possível ocupar o espaço desta lacuna desenvolvendo uma ferramenta de qualidade que responda aos desafios da verificação de sistemas críticos, a partir da fusão de ambas as técnicas ao longo de todo o ciclo de desenvolvimento.