Desarrollo De Software Con Métodos Formales

Desarrollo de Software con Métodos Formales

Características

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.

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 sujeto a herramientas que lo automaticen.

Los métodos formales son un conjunto 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. Ejemplos de métodos formales tenemos las redes Petri, método B, demostración automática de teoremas, RAISE, etc.

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. Los lenguajes 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. El uso de lenguaje de autómatas esta también permitido para aumentar y validar el comportamiento de la aplicación.

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.

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.

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.

Clasificación

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.

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.

• Especificación de comportamiento:

o 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.

o 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.

o 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.

Métodos de Verificación

Entre los métodos de verificación más utilizados, se encuentran:

• Aserciones E/S

• Precondición más débil

• Inducción estructural

Aserciones E/S

Basado en la lógica de Hoare. El programa, en lógica de Hoare, se especifica mediante aserciones que relacionan las entradas y salidas del programa.

...