Rigor Matemático en Ingeniería de Software: Fundamentos y Aplicación de la Especificación Formal

Especificación Formal del Software

Introducción a los Métodos Formales

El concepto se desprende de uno de los niveles de los métodos formales e involucra una serie de técnicas lógicas y matemáticas con las que es posible especificar, diseñar, implementar y verificar los SI (Sistemas de Información). Una especificación formal del software (soft.) es una especificación expresada en un lenguaje cuyo vocabulario, sintaxis y semántica están formalmente definidos. El principal objetivo de la Ingeniería del Software (Ing. del Soft.) es desarrollar sistemas de alta calidad utilizando especificaciones formales.

¿Qué son las Especificaciones Formales?

Es una descripción del sistema que utiliza nociones matemáticas para describir las propiedades de dicho sistema: describe lo que el sistema debe hacer sin decir cómo se va a hacer. El objetivo es permitir la construcción de sistemas que operen confiablemente.

Aplicaciones y Fases del Proceso Formal

Una especificación formal es un proceso que se aplica para desarrollar programas. Estas se utilizan para:

• Políticas de los Requisitos: Definición de un sistema seguro (ej. seguridad como confidencialidad).
• Especificación: Utiliza tablas de lógica.
• Pruebas de Correspondencia entre la Especificación y los Requisitos: Es necesario demostrar que el sistema establece y conserva las propiedades de las políticas de los requisitos.
• Pruebas de Correspondencia entre el Código Fuente y la Especificación: Asegurando la correctitud del código.
• Pruebas de Correspondencia entre el Código Máquina y el Código Fuente.

Las especificaciones formales son técnicas matemáticas rigurosas utilizadas para describir las propiedades de un sistema. El desarrollo de sistemas normalmente implica un proceso de software que puede utilizar el modelo de cascada. Tanto los requerimientos del sistema como el diseño se expresan con detalle y son examinados cuidadosamente antes de la implementación. Uno de los beneficios clave de la especificación formal es la capacidad para descubrir problemas y ambigüedades en los requerimientos del sistema. También ayuda a descubrir problemas en los requerimientos que pueden ser muy costosos de corregir en etapas posteriores.

El Lenguaje Formal

Permite expresar propiedades de un dominio matemático de manera clara y no ambigua. Puede estar basado en la lógica, el álgebra o el cálculo.

Tipos de Especificaciones Formales

Las especificaciones formales se clasifican según su enfoque:

• Especificación Basada en Lógica y Teoría de Conjuntos: Especifican el sistema mediante definiciones formales de estado y operaciones sobre los estados (ej. VDM – Vienna Development Method).
• Especificaciones Algebraicas: Proponen una descripción de estructuras de datos estableciendo tipos y operaciones sobre estos.
• Especificaciones de Comportamiento:
  • Métodos basados en Álgebra de Procesos: Modelan la interacción entre procesos concurrentes (ejecución de múltiples tareas interactivas).
  • Métodos basados en Redes de Petri: (Pre y post condiciones) Describen la evolución del sistema.
  • Basados en la 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.

Beneficios de la Especificación Formal

• Especificación: Una forma de ofrecer garantía al producto es definir con precisión el comportamiento esperado del software. La especificación formal proporciona mayor precisión en el desarrollo del software y los métodos formales brindan las herramientas que pueden incrementar la garantía buscada.
• Verificación: Para asegurar la calidad de los sistemas es necesario probarlos. Para asegurar que se desarrollan pruebas rigurosas se requiere una completa descripción de sus funciones (responde al conjunto de actividades que aseguran que el software implementa correctamente una función específica).
• Validación: Es un conjunto de actividades diferentes que aseguran que el software construido corresponde con los requisitos del cliente.

Ventajas Adicionales de los Métodos Formales

• Mayor productividad.
• Mayor calidad del software.
• Mejor comprensión del sistema.
• Descripción más precisa.
• Aseguramiento matemático de la correctitud.
• Mejora la comunicación con el cliente, ya que dispone de una descripción clara y no ambigua de los requisitos.

Desafíos y Desventajas

• Encarece los productos y ralentiza su desarrollo.
• Los investigadores no conocen la realidad industrial.
• Escasa colaboración entre la industria y el mundo académico.

Conclusión

Se requieren avances y herramientas innovadoras y eficaces para colaborar en la creación del software. Una mejora en las herramientas es totalmente necesaria para mitigar el riesgo de fracaso. El carácter matemático que adquieren las especificaciones formales le permite a los ingenieros analizar y verificar sus modelos. Fija las bases de lo que el producto va a hacer y no de cómo lo hará.