¿Qué es un Método Formal?
Definición: "Método formal es cualquier técnica que trate la construcción y/o el análisis de modelos matemáticos que contribuyen a la automatización del desarrollo de sistemas informáticos"
El papel de los métodos formales en la Ingeniería del Software
Los métodos formales se basan en el empleo de técnicas, lenguajes y herramientas definidos matemáticamente para cumplir objetivos tales como facilitar el análisis y construcción de sistemas confiables independientemente de su complejidad, delatando posibles inconsistencias o ambigüedades que de otra forma podrían pasar inadvertidas.
Los partidarios de los métodos formales defienden que su empleo, a lo largo de todo el ciclo de vida, facilita el desarrollo de especificaciones claras, concisas y no ambiguas, permite el análisis funcional de la especificación y posibilita el desarrollo de implementaciones correctas respecto a su especificación.Sin embargo los detractores aseguran que el empleo de métodos formales supone un volumen de trabajo considerable, aumento en los costes y tiempo de desarrollo y que debe quedar supeditado a herramientas que lo automaticen.
Ventajas de los métodos formales
- Se comprende mejor el sistema.
- La comunicación con el cliente mejora ya que se dispone de una descripción clara y no ambigua de los requisitos del usuario.
- El sistema se describe de manera más precisa.
- El sistema se asegura matemáticamente que es correcto según las especificaciones.
- Mayor calidad software respecto al cumplimiento de las especificaciones.
- Mayor productividad
Problemática actual de los métodos formales
La falta de madurez en la práctica de los métodos formales es la causa de la imposibilidad de utilizarlos a nivel industrial tal y como se utilizan otros métodos de la Ingeniería del Software. Algunas de estas causas son las siguientes:
- 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.
- Los investigadores por lo general no conocen la realidad industrial.
- Es escasa la colaboración entre la industria y el mundo académico, que en ocasiones se muestra demasiado dogmático.
- Se considera que la aplicación de métodos formales encarece los productos y ralentiza su desarrollo.
Conclusión: Los métodos formales se implantarán en la industria probablemente a través de nuevos profesionales con conocimientos sólidos de las técnicas matemáticas.
Aún así, como ya veremos más adelante, los métodos formales están presentes en bastantes campos y no solo los referidos a la ingeniería y la ciencia informática.
Clasificación de los métodos formales
Se pueden encontrar multitud de métodos y técnicas formales con lo que los criterios de clasificación son bastante variados. 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:
- 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.
- Especificaciones algebraicas: proponen una descripción de estructuras de datos estableciendo tipos y operaciones sobre esos tipos.
- 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.
Una especificación escrita en lógica temporal describe las secuencias admisibles de estado (incluyendo estados concurrentes) para el sistema especificado.
