Modelo de Métodos Formales (Procesos del Software).

Métodos Formales

La denominación métodos formales se usa para referirse a cualquier actividad relacionada con representaciones matemáticas del software, incluyendo la especificación formal de sistemas, análisis y demostración de la especificación, el desarrollo transformacional y la verificación de programas. Todas estas actividades dependen de una especificación formal del software.

Una especificación formal del software es una especificación expresada en un lenguaje cuyo vocabulario, sintaxis y semántica están formalmente definidos. Esta necesidad de una definición formal significa que los lenguajes de especificación deben basarse en conceptos matemáticos cuyas propiedades se comprendan bien. La rama de las matemáticas usada es la de matemática discreta, y los conceptos matemáticos provienen de la teoría de conjuntos, la lógica y el álgebra.

En la década de los 80, muchos investigadores de ingeniería del software propusieron que el uso de métodos formales de desarrollo era la mejor forma de mejorar la calidad del software. Argumentaban que el rigor y el análisis detallado, que son una parte esencial de los métodos formales, podrían dar lugar a programas con menos errores y más adecuados a las necesidades de los usuarios. 

Fuente: http://tema3isoftware.blogspot.com/p/modelo-de-metodos-formales.html

Ventajas y Desventajas

Ventajas

1. Se comprende mejor el sistema.
2. La comunicación con el cliente mejora ya que se dispone de una descripción clara y no ambigua de los requisitos del usuario.
3. El sistema se describe de manera más precisa.
4. El sistema se asegura matemáticamente que es correcto según las especificaciones.
5. Mayor calidad software respecto al cumplimiento de las especificaciones.
6. Mayor productividad

Desventajas 

1. El desarrollo de herramientas que apoyen la aplicación de métodos formales es complicado y los programas resultantes son incómodos para los usuarios.
2. Los investigadores por lo general no conocen la realidad industrial.
3. Es escasa la colaboración entre la industria y el mundo académico, que en ocasiones se muestra demasiado dogmático.
4. Se considera que la aplicación de métodos formales encarece los productos y ralentiza su desarrollo

Clasificación

La clasificación más común se realiza en base al modelo matemático subyacente en cada método, de esta manera podrían clasificarse en:

1. Especificaciones basadas en lógica de primer orden y teoría de conjuntos: permiten especificar el sistema mediante un concepto formal de estados y operaciones sobre estados. Los datos y relaciones/funciones se describen en detalle y sus propiedades se expresan en lógica de primer orden. La semántica de los lenguajes está basada en la teoría de conjuntos. Los métodos de este tipo más conocidos son: Z, VDM y B.
2. Especificaciones algebraicas: proponen una descripción de estructuras de datos estableciendo tipos y operaciones sobre esos tipos. Para cada tipo se define un conjunto de valores y operaciones sobre dichos valores. Las operaciones de un tipo se definen a través de un conjunto de axiomas o ecuaciones que especifican las restricciones que deben satisfacer las operaciones. Métodos más conocidos: Larch, OBJ, TADs.
3. Especificación de comportamiento:

• Métodos basados en álgebra de procesos: modelan la interacción entre procesos concurrentes. Esto ha potenciado su difusión en la especificación de sistemas de comunicación (protocolos y servicios de telecomunicaciones) y de sistemas distribuidos y concurrentes. Los más conocidos son: CCS,CSP y LOTOS.
• Métodos basados en Redes de Petri: una red de petri es un formalismo basado en autómatas, es decir, un modelo formal basado en flujos de información. Permiten expresar eventos concurrentes. Los formalismos basados en redes de petri establecen la noción de estado de un sistema mediante lugares que pueden contener marcas. Un conjunto de transiciones (con pre y post condiciones) describe la evolución del sistema entendida como la producción y consumo de marcas en varios puntos de la red.
• Métodos basados en lógica temporal: se usan para especificar sistemas concurrentes y reactivos. Los sistemas reactivos son aquellos que mantienen una continua interacción con su entorno respondiendo a los estímulos externos y produciendo salidas en respuestas a los mismos, por lo tanto el orden de los eventos en el sistema no es predecible y su ejecución no tiene por qué terminar.

Fuente: http://es.wikipedia.org/wiki/M%C3%A9todo_formal