Proyecto : Verificación formal automatizada de un marcapasos

Informe de avance a febrero del 2002

Luis Sierra

I. Datos del proyecto

Nombre del Proyecto: Verificación formal automatizada de un marcapasos

Responsable: Luis Ricardo SIERRA ABBATE

Tutor: Cristina Roxana CORNES BOQUETE

Área: Tecnológica

Grado y Horas del responsable: Grado 3, 40 horas

Instituto: Computación (InCo)

Facultad: Ingeniería

Fecha de finalización Julio del 2002

II. Informe de avance

Este informe es acumulativo con el presentado en Octubre del 2001, y va acompañado de una copia del mismo.

Principales actividades realizadas

En los últimos meses se ha realizado una presentación en el InCo acerca de distintas perspectivas para el estudio de sistemas temporizados. En cuanto al modelado del sistema en estudio, se ha pasado a emplear la herramienta UppAal (en lugar de Kronos) principalmente debido a su interfase gráfica.

Avances

  1. Análisis del microcontrolador. Familiarización con el problema.

    1. Estudio del problema concreto, realizado de acuerdo a las técnicas habituales para el relevamiento y análisis de problemas.

    Fase terminada.

  2. Elaboración de una especificación formal del microcontrolador, por medio de:

    3. Fase terminada.

  3. Análisis del código

    4. La reconstrucción del modelo a partir del código está en proceso de realización. Para construir el mismo se emplea la herramienta UppAal, debido a su interfase gráfica y a que soporta definición de variables enteras. A la fecha solamente se dispone de los niveles superiores de la implementación en dos modos de operación. La verificación de las propiedades de interés será posible cuando se finalicen todos los niveles de la programación del controlador.

  4. Comparación y acercamiento entre los ítems 2 y 3.

    5. Está pendiente.

  5. Análisis comparativo de las herramientas utilizadas.

    6. El trabajo detallado con otras herramientas de especificación (Spin, UppAal, Kronos) permite realizar un cierto nivel de comparación a nivel de usuario. Como el trabajo se ha realizado en distintas plataformas, no se puede dar una comparación cuantitativa ni siquiera en los casos en que se han verificado las mismas propiedades. La perspectiva consiste en realizar las comparaciones de eficiencia en cuanto se disponga de la máquina específica para realizar dicha tarea. Cualitativamente, se pueden establecer los siguientes puntos:

    • UppAal y Kronos están orientados a la verificación de sistemas de tiempo real.
    • El empleo de interfase gráfica integrada en UppAal facilita el modelado de los sistemas.
    • Los diagramas de transición generados por Spin permiten un seguimiento adecuado de las comunicaciones en el momento de ejecución.

  6. Caracterización de la metodología empleada.

    7. En desarrollo.

  7. Elaboración de documentación.

    8. Se realizó una presentación acerca de distintas ópticas para tratar el estudio del tiempo en las Jornadas de Informática e Investigación Operativa del InCo.

Diferencias con lo planeado

La tarea de recontrucción del modelo ha insumido mayor tiempo del esperado. La comunicación con los productores del software no se han mantenido en el nivel deseado, debido a estas demoras. Por otro lado, ha surgido la posibilidad de iniciar trabajos conjuntos con el laboratorio Verimag, Grenoble, lo que puede modificar algunas de las actividades planteadas.

 
 
 
 
----------------------- -----------------------
Responsable Tutor