Método formal
En ingeniería de software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos.[1] Los métodos formales se caracterizan por emplear técnicas y herramientas matemáticas para lograr una facilitación a la hora de encarar la construcción o el análisis de un modelo matemático de un sistema.[2]
Historia
En 1967, Robert Floyd propuso utilizar lo que se denominó método de aserciones intermedias como una manera de estudiar las propiedades de los programas. Destacó la posibilidad de definir la semántica de las operaciones mediante reglas lógicas afirmando que estas aserciones son válidas después de ejecutarse las operaciones basándose en la información de las aserciones que son válidas antes de ejecutarse dichas operaciones.
Estas ideas fueron perfeccionadas por Hoare dando lugar al método axiomático (precondiciones E/S) donde introdujo la idea de "invariante".
En 1976, Edsger Dijkstra, presentó un método formal llamado precondición más débil, basado en la transformación de predicados wp (weakest precondition). De esta manera rompía con las ideas de verificación a posteriori de Floyd y Dijkstra. La idea principal era invertir los métodos de ambos de tal manera que se pudiera derivar la precondición a partir de la postcondición.
Ventajas
Ventajas
- 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 en el software respecto al cumplimiento de las especificaciones.
- Mayor productividad.
Desventajas
- 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.
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 específica mediante aserciones que relacionan las entradas y salidas del programa. Se garantiza que si la entrada actual satisface las restricciones de entrada (precondiciones) la salida satisface las restricciones de salida (poscondiciones).
Se utiliza una expresión del tipo P{programa}Q, siendo P y Q aserciones de la lógica, para indicar que si P es cierto antes de la ejecución del programa y dicho programa termina, entonces Q es cierto tras la ejecución de dicho programa. Este método permite tanto la corrección parcial como total de los programas.
Un caso especial son los bucles, donde los predicados deben mostrar una relación invariante, es decir, deben ser ciertos independientemente del número de vueltas del bucle, por lo tanto el predicado debe cumplir lo siguiente:
- Es cierto a la entrada del bucle
- Es cierto en cualquier paso del bucle
- Junto con la negación de la condición del bucle, implica que el predicado se cumple a la salida del bucle.
Precondición más débil
Básicamente, consiste en dada una poscondición POST, encontrar, operando hacia atrás, un programa S tal que wp(S, POST) (la precondición) se satisfaga en un amplio conjunto de situaciones
Dada una proposición (P) S (Q) donde S es un conjunto de sentencias de un módulo de un programa, y donde P y Q son los predicados que se cumplen antes y después de S respectivamente, se dice que P es la precondición más débil (wp) de S, si es la condición mínima que garantiza que Q es cierto tras la ejecución de S.
Inducción estructural
La inducción estructural es una técnica de verificación formal que se basa en el principio de inducción matemática.
Dado un conjunto S con una serie de propiedades y una proposición P que se desea probar, la inducción matemática:
- Demuestra que P es cierto para el mínimo número de elementos (o casos triviales) de S.
- Asume que P es cierto para un número de elementos (o casos posibles) de S menores o iguales a N.
- Demuestra que entonces P es cierto para el elemento N+1 de S.
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:
- 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:
- 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.
Véase también
Referencias
- R. W. Butler (6 de agosto de 2001). «What is Formal Methods?». Consultado el 16 de noviembre de 2006.
- C. Michael Holloway. . 16th Digital Avionics Systems Conference (27–30 October 1997). Archivado desde el original el 16 de noviembre de 2006. Consultado el 16 de noviembre de 2006.
Bibliografía
- Jean François Monin and Michael G. Hinchey, Understanding formal methods, Springer, 2003, ISBN 1-85233-247-6.
- Jonathan P. Bowen and Michael G. Hinchey, Formal Methods. In Allen B. Tucker, Jr. (ed.), Computer Science Handbook, 2nd edition, Section XI, Software Engineering, Chapter 106, pages 106-1 – 106-25, Chapman & Hall / CRC Press, Association for Computing Machinery, 2004.
- Michael G. Hinchey, Jonathan P. Bowen, and Emil Vassev, Formal Methods. In Philip A. Laplante (ed.), Encyclopedia of Software Engineering, Taylor & Francis, 2010, pages 308–320.
Enlaces externos
- Formal Methods Wiki
- List of formal methods and tools
- Formal methods publications
- Who's who in formal methods
- Foldoc:formal methods
- soportado por el proyecto DEPLOY