Metodología para la construcción de software correcto

Abstract

En los últimos diez años han aparecido herramientas para la verificación formal de programas que están entre los verificadores completamente automáticos y los verificadores que aceptan entrada del usuario en todos los pasos de prueba. Estas herramientas, conocidas como verificadores auto-active, acercan la verificación formal a una mayor audiencia en parte porque el usuario interactúa con el verificador a nivel del lenguaje de programación. Aun así, el programador convencional que quiera echar un vistazo y experimentar los beneficios de la verificación formal antes de profundizar en el tema, deberá invertir una considerable cantidad de tiempo en aprender teorías, técnicas y herramientas, muchas de las cuales están dispersas. Por otra parte, la criticidad de los sistemas que aparecerán en el futuro demandará profesionales con conocimientos en métodos formales, razón por la cual parece importante elaborar material didáctico en esta disciplina. En este trabajo se propone acercar gradualmente al programador convencional a la verificación formal. Para ello, se presentan problemas que posteriormente se resuelven utilizando teorías, técnicas y herramientas que seleccionadas alivian algunas dificultades iniciales.