Informatica

Métodos formales en el desarrollo de software


Especial para INFORMÁTICA

I PARTE DE II

Los métodos formales han surgido como enfoques analíticos donde el desarrollo de software puede ser verificado por medio de teorías matemáticas, aportando ventajas en la calidad del software.
La calidad del software es uno de los problemas más importantes en los procesos de desarrollo del mismo. El garantizar el correcto funcionamiento y desempeño bajo situaciones no determinadas es una tarea que se tiene que realizar con muchísimo cuidado.
En este artículo se pretende encausar a los lectores en el uso de los métodos formales para el desarrollo de software, a través de una serie de consideraciones relevantes al tomar decisión en hacer uso de dicha metodología.

¿Qué son los métodos formales?
Los métodos formales son un conjunto de tendencias de desarrollo de software y hardware en donde la especificación, verificación y diseño de componentes se realiza mediante notaciones, lenguajes, herramientas y técnicas basadas en teorías con sólido fundamento matemático.
El uso de notaciones y lenguajes formales permite plantear de manera clara los requerimientos de un sistema, generando especificaciones que definen el comportamiento en términos del “qué debe hacer” y no del “cómo lo hace”. Gracias al correcto proceso de especificación, propiedades derivadas de cada módulo pueden ser verificadas mediante técnicas de razonamiento asociadas a los modelos formales, como probadores de teoremas y verificadores de modelos.
A partir de las especificaciones, la implementación de un sistema puede ser generada de manera casi automática. Es necesario bajar en el grado de abstracción de las especificaciones mediante técnicas como refinamiento o concretización. En este proceso, denominado diseño formal, es necesario garantizar que cada nivel de abstracción generado cumpla con las propiedades verificadas en los grados en las abstracciones de más alto nivel.
En los procesos de especificación, hay corrientes identificables en los lenguajes de especificación formal. Los más conocidos y utilizados son Z y VDM, los cuales han sido recomendados como un estándar oficial para la especificación en la construcción de sistemas de software.
Para los procesos de verificación, dos grandes enfoques son reconocidos: los verificadores de modelos, que realizan una búsqueda exhaustiva sobre los estados posibles de una especificación para encontrar posibles fallas no consideradas, y los probadores de teoremas, en donde la especificación y sus propiedades deseables se formalizan como fórmulas lógicas, y se prueban mediante una serie de axiomas y reglas de inferencia presentes en cada probador.
Los métodos formales difieren en la manera y tiempos de cada una de las fases del ciclo de vida del software. Su utilización requiere mayor tiempo en el desarrollo de especificación y la construcción de diseños correctos.
* Profesor titular del Dep. de Computación, Facultad de Ciencias e Ingeniería
Unan, davenda69@hotmail.com.