¿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.
En los últimos años, la idea de que la formalización matemática del SW es el enfoque más apropiado para conseguir mejorar su calidad va adquiriendo cada vez más fuerza. 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.
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.
