Técnicas formales para el desarrollo jerárquico de sistemas concurrentes

Abstract

SE PRESENTA UN METODO PARA EL DESARROLLO DE SISTEMAS CONCURRENTES, APLICABLE A SISTEMAS QUE INERACICIONAN CON SU ENTORNO ENVIANDO Y RECIBIENDO MENSAJES, LA ESPECIFICACION DE UN SISTEMA ESTA DADA POR UNA FAMILIA DE VARIABLES DE ESTADO QUE REPRESENTAN LOS ESTADOS DEL SISTEMA; UNA FAMILIA DE REGLAS DE TRANSICION QUE DESCRIBEN EL CAMBIO DE ESTADO QUE TIENE LUGAR CON CADA OPERACION DE COMUNICACION; UNA FAMILIA DE GUARDAS, QUE JUNTO CON LAS ANTERIORES, DESCRIBEN LAS SECUENCIAS DE COMUNICACIONES POSIBLES; UNA FAMILIA DE REGLAS DE VITALIDAD QUE DESCRIBEN CIERTAS PROPIEDADES DEL SISTEMA. SE INCLUYE TAMBIEN UNA NOCION DE IMPLEMENTACION DISTRIBUIDA Y SE PRESENTAN TECNICAS PARA ESTABLECER FORMALMENTE SU CORPECCION. LA SEMANTICA DE LAS ESPECIFICACIONES CON VARIABLES DE ESTADO SE ESTABLECEN EMPLEANDO UN MODELO MATEMATICO DE LOS PROGRAMAS PARALELOS AMPLIAMENTE DIFUNDIDO: EL MODLO DE FALLOS. SE DEFINEN UNA REPRESENTACION DE DICHO MODELO EMPLEANDO UNA CLASE PARTICULAR DE AUTOMATAS, LOS LLAMADOS AUTOMATAS DE ACEPTACION. DICHA REPRESENTACION PRPORCIONA TAMBIEN LAS BASES PARA LA CONSTRUCCION DE HERRAMIENTAS DE VERIFICACION AUROMATICA DE SISTEMAS CONCURRENTES, CUANDO EL NUMERO DE ESTADOS ES FINITO. LA UTILIDAD DEL METODO PROPUESTO SE ILUSTRA MEDIANTE SU APLICACION EN DIVERSOS EJEMPLOS NO TRIVIALES.