I DATOS DEL PROYECTO

A) Nombre del Proyecto:

Verificación de Sistemas Reactivos y de Tiempo Real en Teoría de Tipos

B) Responsable: Carlos Daniel Luna Garcia

Nombre del Tutor: Dr. Gustavo Betarte

C) Servicio Universitario: Facultad de Ingeniería, U. de la República

D) Departamento o Institución: Instituto de Computación

DETALLE DE LA EJECUCION DE RECURSOS (en U$S)
 

Detalle de Gastos efectuados	Monto
En todo concepto	4000

E) Difusión
 

Publicaciones/otros	Monto
Carlos Luna. "Análisis de Sistemas de Tiempo Real en Teoría de Tipos. Una Metodología de Trabajo". 5o Workshop Iberoamericando de Ingeniería de Requisitos y Ambientes de Software. IDEAS’2002, La Habana, Cuba, 23 al 26 de Abril de 2002.
Carlos Luna, P. Martellotto, M. Bongiovanni, M. M. Novaira. "Teoría de Tipos y Coq en la enseñanza de Programación Funcional e Imperativa". CACIC'2001, El Calafate, Santa Cruz, Argentina, 16-20 de Octubre de 2001.
Carlos Luna. "De especificaciones declarativas a programas eficientes. Un caso de estudio". En proceedings de las Jornadas Chilenas de Computación, Universidad de Magallanes, Punta Arenas, Chile, 5-9 Noviembre de 2001.
Carlos Luna. "Una Generalización del Modelo AGM de Cambio de Creencias", publicado en Inteligencia Artificial, Revista Iberoamericana de Inteligencia Artificial. No.13 (2001), pp. 23-32. ISSN: 1137-3601. © AEPIA (http://www.aepia.dsic.upv.es/).
Carlos Luna. Informe técnico preliminar: "Verificación de Sistemas Reactivos y de Tiempo Real en Teoría de Tipos". Instituto de Computación, Fac. de Ingeniería, U. de la República.

Actualmente se encuentran sometidos dos artículos para referato y un tercero está en proceso de redacción con docentes de Argentina.

1. Realice un informe de todas las actividades desarrolladas.

• Informe con:

• Formalizaciones genéricas de sistemas reactivos y de tiempo real en teoría de tipos, usando Coq.
• Análisis de las posibilidades y limitaciones para trabajar con sistemas de tiempo real en Coq usando tiempo discreto y tiempo continuo, y las relaciones entre ambas estructuras temporales en la verificación de los sistemas.
• Análisis de extensiones del lenguaje de descripción de los sistemas de tiempo real –usando grafos temporizados– con estructuras de datos y una extensión que permita trabajar con grafos temporizados más generales que consideren asignaciones a los relojes de valores no necesariamente constantes.
• Análisis preliminar de mecanismos de síntesis de programas reactivos y de tiempo real.

• Desarrollo de tácticas particulares para la simplificación de pruebas deductivas de propiedades sobre los sistemas especificados en Coq. Las tácticas abarcan fundamentalmente dos clases importantes de propiedades: invarianza y alcanzabilidad.

• Desarrollo de bibliotecas con operadores temporales para las lógicas CTL y TCTL. Análisis y prueba de propiedades de los operadores para razonar sobre sistemas reactivos y de tiempo real. Estas bibliotecas han sido incorporadas al proyecto Coq del INRIA, Francia, con el nombre CTL_TCTL (http://Coq.inria.fr/).
• Creación de la biblioteca RailRoad_Crossing_Example del proyecto Coq del INRIA (http://Coq.inria.fr/). Esta biblioteca contiene la modelización y verificación de un benchmark en el área de los sistemas de tiempo real.

• Desarrollo de una metodología de trabajo que permita compatibilizar el uso del asistente de pruebas Coq y el model checker Kronos en la especificación, el análisis y eventualmente la síntesis de sistemas reactivos y de tiempo real.

• Desarrollo y publicación del artículo:

• Desarrollo del curso de grado y de postgrado (conjuntamente con la Dra. Nora Szasz): "Construcción formal de programas en teoría de tipos usando Coq". Segundo semestre de 2001, Universidad Nacional de Río Cuarto (UNRC), Río IV, Córdoba, Argentina. En este marco, se formó un grupo de trabajo entre docentes de Argentina y Uruguay. Algunos resultados alcanzados, que se vinculan directamente con los objetivos del proyecto de iniciación a la investigación de quien suscribe, son:

• Intercambio de docentes y estudiantes entre la UNRC y la Universidad de la República para realizar cursos e iniciar trabajos de maestría. Actualmente dos estudiantes de la UNRC se encuentran inscriptos en la maestría del PEDECIBA Informática –Uruguay– y realizaron tareas de formación en el área de métodos formales (en particular, tomaron el curso "Construcción formal de programas en teoría de tipos usando Coq").
• Desarrollo y publicación del trabajo: "Teoría de Tipos y Coq en la enseñanza de Programación Funcional e Imperativa". Carlos Luna, P. Martellotto, M. Bongiovanni, M. M. Novaira. CACIC'2001, El Calafate, Santa Cruz, Argentina, 16-20 de Octubre de 2001.
• Desarrollo del artículo "Teoría de Tipos y Coq en la Enseñanza de Programación Funcional e Imperativa. Taller de Construcción Formal de Programas". Carlos Luna, P. Martellotto, M. M. Novaira. A ser sometido a evaluación en el X Congreso Iberoamericano de Educación Superior en Computación, CIECS’2002, dentro de la Conferencia Latinoamericana de Educación Superior en Computación, Uruguay, Noviembre de 2002.
• Incorporación de quien suscribe al proyecto de investigación: Verificación y desarrollo de sistemas en un contexto relacional. Proyecto de Ciencia y Técnica, UNRC, Argentina, bajo la dirección del C.C Gabriel Baum (Lifia, UNLP, Argentina). Este proyecto comparte objetivos comunes con los planteados en el presente proyecto de iniciación a la investigación.

• Desarrollo y publicación de los trabajos:

• Carlos Luna. "De especificaciones declarativas a programas eficientes. Un caso de estudio". En proceedings de las Jornadas Chilenas de Computación, Universidad de Magallanes, Punta Arenas, Chile, 5-9 Noviembre de 2001.
• Carlos Luna. "Una Generalización del Modelo AGM de Cambio de Creencias", publicado en Inteligencia Artificial, Revista Iberoamericana de Inteligencia Artificial. No.13 (2001), pp. 23-32. ISSN: 1137-3601. © AEPIA (http://www.aepia.dsic.upv.es/).

Las fases planteadas en la beca fueron realizadas en un porcentaje alto. Las tareas que no lograron ser llevadas a cabo en su totalidad se describen a continuación:

• Analizar "en detalle" la construcción y corrección, en teoría de tipos, de abstracciones de sistemas reactivos y de tiempo real, a fin de demostrar ciertas propiedades sobre sistemas más reducidos (abstractos), que puedan ser luego generalizadas a los sistemas originales.
• Analizar "en detalle" mecanismos de síntesis de programas reactivos y de tiempo real en teoría de tipos, usando las ventajas del asistente de pruebas Coq, que permite expresar las nociones de prueba y programa en una teoría unificada.
• Analizar y desarrollar "con más detalle" una extensión del lenguaje de descripción de los sistemas de tiempo real –usando grafos temporizados– con estructuras de datos y en particular aquellas con dominios infinitos.

• se priorizaron otras tareas, no planificadas inicialmente. Estas tareas fueron descriptas en el inciso A precedente.
• se priorizó la publicación de artículos.

• Desarrollo de bibliotecas con operadores temporales para las lógicas CTL y TCTL. Análisis y prueba de propiedades de los operadores para razonar sobre sistemas reactivos y de tiempo real. Incorporación de estas bibliotecas al proyecto Coq del INRIA, Francia, con el nombre CTL_TCTL (http://Coq.inria.fr/).
• Creación de la biblioteca RailRoad_Crossing_Example del proyecto Coq del INRIA (http://Coq.inria.fr/). Esta biblioteca contiene la modelización y verificación de un benchmark en el área de los sistemas de tiempo real.

• Informe preliminar detallado en el inciso A, que se adjunta a este informe técnico.
• Las cuatro publicaciones referidas en el inciso A.
• Las tres publicaciones pendientes. Dos sometidas a evaluación y una en proceso de redacción.

• El desarrollo del curso de grado y de postgrado (conjuntamente con la Dra. Nora Szasz): "Construcción formal de programas en teoría de tipos usando Coq". Segundo semestre de 2001, Universidad Nacional de Río Cuarto (UNRC), Río IV, Córdoba, Argentina. En este marco, se formó un grupo de trabajo entre docentes de Argentina y Uruguay. En el inciso A se mencionan los principales resultados alcanzados de esta experiencia, que se vinculan con los objetivos del proyecto de iniciación a la investigación de quien suscribe.

• Las bibliotecas incorporadas al proyecto Coq del INRIA pueden ser utilizadas por la comunidad científica como base para la especificación y el análisis formal de sistemas reactivos y de tiempo real.
• Los informes y las publicaciones que se derivan de ellos permiten ampliar el conocimiento en el área de la verificación de los sistemas reactivos y de tiempo real en el paradigma deductivo y su vinculación al área de la verificación automática de estas clases de sistemas.
• La metodología de trabajo propuesta en este permite compatibilizar el uso del asistente de pruebas Coq y un model checker como Kronos en la especificación y el análisis de sistemas reactivos y de tiempo real. Debido a que los model chekers son ampliamente utilizados en la industria para verificar estas clases de sistemas, esperamos que la metodología introducida en este trabajo tenga un impacto positivo tanto en el ámbito académico como el industrial, ya que la integración (aunque parcial) de los dos modelos permite salvar las limitaciones de cada enfoque, potenciando las virtudes de cada uno de ellos.
• En relación a la vinculación con la UNRC, Argentina, esperamos que esta experiencia sirva de base para estrechar relaciones fructíferas de aquí en más con la Universidad de la República, Uruguay. En este sentido, se creó un proyecto de investigación conjuntamente con la UNRC, se está desarrollando un paper compartido, se está planificando un curso para el segundo semestre de 2002 y se logró incorporar a dos docentes de la UNRC en postgrados del PEDECIBA informática.

Se incluyen anexos.

F) Otras consideraciones y/o recomendaciones que Ud. considere pertinente realizar.

Este trabajo está enmarcado en la actividad de investigación desarrollada por el proyecto seleccionado y financiado CSIC "integración de teoría de tipos y verificación de modelos para la certificación formal de sistemas reactivos", cuyos responsables científicos son el Dr. Gustavo Betarte y la Dra. Cristina Cornes, del grupo de Métodos Formales del Instituto de Computación de la Universidad de la República (Uruguay).

RESUMEN DEL PROYECTO

INFORME COMPLETO (.pdf)