CONTRATO PROGRAMA PARA PROYECTOS INSTITUCIONALES A

CARGO DE LA COMISIÓN SECTORIAL DE INVESTIGACIÓN CIENTIFICA

(UNIDAD COORDINADORA DEL PROYECTO INSTITUCIONAL, UCPI)

 



 

1. Compromiso


Con la firma del presente documento la Unidad Operativa se compromete ante la UCPI a ejecutar las acciones especificadas que se detallan.


2. Contenido del compromiso


El contenido del compromiso que asume la Unidad Operativa es el que surge de las especificaciones reseñadas en el ítem 6, donde se indican las acciones previstas, los plazos de ejecución y los resultados esperados de dichas acciones.


3. Conformidad


En señal de conformidad, el responsable de la UCPI. Ing. Enrique Cabaña y el responsable de la Unidad Operativa Luis Sierra suscriben tres ejemplares del presente Contrato Programa.


4. Identificación del Proyecto


 

5. Justificación y Antecedentes (hasta 150 palabras)


Acompañar el esfuerzo nacional para asegurar el fortalecimiento de la base de recursos humanos, el establecimiento de instituciones científicas, la mejora y actualización de la educación científica, la integración de la ciencia a la cultura nacional, el desarrollo de la infraestructura y la promoción de la tecnología y de las capacidades de innovación. Este objetivo general traduce también al plano local recomendaciones principales del Congreso Mundial de Ciencia patrocinado por UNESCO. (Budapest 1999).


La Universidad intensificará su acción -como parte de un necesario esfuerzo nacional mancomunado- para incorporar el conocimiento a las actividades sociales y productivas, contribuyendo de esa manera a que nuestro país disponga recursos para la generación de tecnologías y lograr por esa vía un adecuado desarrollo social, económico y cultural.


Para estimular, la innovación se requiere establecer vínculos entre las distintas áreas del conocimiento y una constante interacción entre los diferentes actores. Los conocimientos y la experiencia acumulada de la Universidad deben mantenerse abiertas a la demanda mediante una adecuada información pública. De esta manera se facilitará la necesaria participación de los científicos en los programas que tengan por objeto el desarrollo social y productivo armónico del país.


Finalmente, en el contexto de los desafíos del desarrollo científico y tecnológico actual, es esencial enfatizar que la Universidad de la República debe velar por un desarrollo armonioso de la capacidad de creación original en todos los ámbitos, única garantía de un crecimiento sustentable y que atienda a las necesidades fundamentales de la sociedad y a la afirmación de la dignidad humana.



6. Especificaciones del Proyecto Financiado


6.1 Objetivos generales.


Hoy por hoy numerosas empresas productoras de software desarrollan aplicaciones críticas que ponen en juego vidas humanas y/o grandes inversiones económicas. La informática médica o el comercio electrónico por Internet son sólo dos ejemplos de tales aplicaciones. Existe, por lo tanto, una real necesidad de desarrollar metodologías y herramientas que permitan asegurar de manera rigurosa que tales programas son enteramente confiables. Esta afirmación no está basada exclusivamente en razones de seguridad. Desde un punto de vista económico, la detección tardía de un error de programación puede cuestionar decisiones de diseño ya tomadas. El costo de estos errores es considerado el mayor en todas las etapas del proceso de desarrollo de sistemas informáticos.


Las normas internacionales de calidad imponen hoy la verificación de código como etapa obligatoria del desarrollo de software. Por otra parte, la comunidad científica ha invertido un considerable esfuerzo en proponer técnicas de verificación formal de programas y herramientas que las implementen. El desafío planteado hoy es continuar el desarrollo de dichas herramientas,y experimentar e integrar las técnicas propuestas, buscando dar respuesta a las necesidades actuales de la industria.


En Uruguay se desarrollan aplicaciones informáticas críticas. En este contexto, existe un interés explícito por parte de la empresa CCC en aplicar técnicas formales para el estudio de la corrección del código de microcontroladores utilizados en marcapasos. La certificación matemática de la correctitud de sistemas informáticos de esta índole, empleando intensivamente herramientas automáticas constituye el núcleo alrededor del cual se comprende el presente proyecto.


6.2 Objetivos específicos de las acciones financiadas.


Son objetivos específicos del mismo los siguientes:

  1. Uso integrado de distintos puntos de vista sobre la verificación automática. Esto implica desarrollar una estrategia que aproveche las diferencias entre los distintos enfoques y herramientas, buscando complementariedades entre ellos.
  2. Comparación entre ambos puntos de vista, desde la siguiente perspectiva de la expresibilidad de las propiedades del sistema.
    Cabe aclarar que esta comparación es importante a los fines de identificar las mejores decisiones de diseño de la nueva metodología a desarrollar.
  3. Validación del software crítico concreto. Si se encontraran errores en el mismo, se esperan obtener, además, al menos alguno de los siguientes puntos:
    1. ejemplos que muestren la incorrectitud del software.
    2. estrategias para reparar el sistema.
    3. un nuevo software correcto.

6.3 Acciones previstas (hasta 150 palabras)


La estrategia a llevar adelante durante este proyecto tendrá presenta las siguientes características:


En consecuencia, la estrategia propuesta considera importante la continuidad del docente responsable en el GMF dentro del Instituto de Computación, así como de su vinculación con investigadores de otros centros de investigación.


La vinculación con el medio productivo e industrial será central a lo largo del mismo. No solamente se mantendrá un diálogo fluído con la empresa CCC, sino que se espera iniciar nuevos contactos con empresas e instituciones que estén reconociendo la necesidad del uso de métodos formales para su mejor desarrollo. También será considerada importante la participación en instancias no académicas que den a conocer los alcances de esta propuesta.


El trabajo concreto se desarrollará sobre los siguientes ejes:




6.4 Plazos de ejecución (indicar los plazos con la mayor precisión posible, hasta 75 palabras)


La realización del proyecto en el ejercicio año 2001. En el período se realizarán estudios comparativos de distintas herramientas y se establecerá la mejor vinculación entre éstas y el software problema. Con ese fin se invertirá en equipo computacional adecuado. Luego se realizará la verificación del software, y se implementarán utilitarios para la integración de herramientas con dicho fin.


6.5 Calendario financiero y distribución por rubro.

Período

Sueldos

Gastos

Inversiones

Total

01-08-01 31-12-01

$ 32.941.80

$ 1.778.20

$ 35.000

$ 69.720



6.6 Resultados esperados de las acciones (indicar resultados concretos esperados de las acciones, hasta 150 palabras)

Los resultados que se esperan de este proyecto son:

  1. Comparción a través del caso de estudio del marcapasos de distintas herramientas de verificación de modelos. La comparación se realizará sobre los aspectos de especificación y prueba del sistema, en términos de
    1. expresividad del lenguaje de especificación: por ejemplo, identificar que clase de problemas resulta más fácil describir en cada una.
    2. eficiencia de las distintas herramientas.
    3. ergonomía de las herramientas: es decir, cuán fácil son de usar.
  2. Desarrollo de una metodología que permita transitar desde la especificación de un problema hasta su codificación en un lenguaje de programación, y en sentido inverso, en el contexto de la verificación automática de sistemas.
  3. Verificación del código fuente del marcapasos tratando de evitar modelizaciones indirectas. Es decir, el programa a verificar debe ser exactamente el programa a ejecutar.

  4. Implementación de utilitarios que habiliten a un uso integrado de distintas herramientas de verificación.


Firma Responsable UCPI
Firma Responsable Unidad Operativa






ACLARACIONES