Descripción incremental de sistemas basada en el cálculo de refinamientos y lógicas modales ejecutables:
Aplicaciones a los sistemas de seguridad crítica


Proyecto CICYT TIC94-0847-C02-02



Resumen

La investigación conducente al desarrollo de software seguro y fiable que pueda ser utilizado en aplicaciones tales como Bases de Datos Temporales activas, Sistemas de Seguridad Crítica y Sistemas Multiagentes, tiene gran interés científico e industrial. Existen sistemas comerciales de gestión de especificaciones y programas, pero carecen de una rigurosa base formal y por tanto están limitados en cuanto a generalidad y fiabilidad.

Por otra parte, los sistemas formales para la especificación de requerimientos que existen, sólo se han aplicado a pequeños problemas o a limitados aspectos de la captura de requerimientos. En este proyecto se apuesta, en primer lugar, por la aplicación de las técnicas de la lógica computacional a la especificación de requerimientos de problemas reales como son los mencionados, especialmente los Sistemas de Seguridad Crítica.

En el subproyecto 1, entendemos esta tarea como un proceso de refinamiento entre varios niveles de detalle de la especificación del sistema. En cada etapa es posible comprobar propiedades y la coherencia de una versión respecto a la anterior en el proceso de refinamiento. Una vez completa la especificación se podrán aplicar métodos de transformación hacia programas más eficientes. Esta metodología está fundada en un lenguaje de especificación básico (COR), rigurosamente fundamentado y fácil de entender, apto para su extensión incremental según las necesidades del usuario.

En el subproyecto 2, entendemos que, en el área de los Sistemas de Seguridad Crítica, los lenguajes neutrales respecto al fenómeno en el dominio del problema, no se adecúan a la axiomatización del conocimiento. Por lo tanto, son necesarios lenguajes de programación que permitan la representación de este conocimiento sobre el dominio y, debido a que las aplicaciones consideradas tienen en común la necesidad de razonar sobre conocimiento, tiempo y creencia, es bastante aceptado que los lenguajes requeridos han de ser lenguajes basados en lógicas modales y temporales. Con esta visión, adoptamos como punto de partida para la búsqueda de mecanimos de ejecución, formas ejecutables de lenguajes modales y temporales (LMex), siguiendo técnicas bien contrastadas.