Metodo formalista

* 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"* 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 yteorí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 seexpresan 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: proponenuna 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 untipo 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 decomunicació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 unformalismo 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 deestado 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...