Este documento informa de las actividades llevadas a cabo durante el proyecto de iniciación a la investigación Verificación formal automatizada de un marcapasos e indica posibles caminos para posteriores estudios y desarrollos.
Podemos distinguir tres puntos diferentes en el proyecto. El primero consistió en la especificación del problema a tratar. Un segundo punto fue el planteo de propiedades de seguridad concernientes al código empleando marcos lógicos. El código a estudiar consistía del programa usado efectivamente, codificado en un dialecto C que incorpora características propias de la programación de microprocesadores. El tercer punto, el uso de técnicas de análisis estático a fin de especificar y demostrar propiedades sobre el código de estudio. Estos últimos dos puntos se solapan fuertemente. Consisten de ópticas diferentes para acercarse al problema medular de la verificación de código.
Este punto se distingue de los otros en que formaliza un problema establecido intuitivamente. De esta manera se eliminan ambigüedades en el planteo de las propiedades a probar. En los restantes puntos se estudia un objeto formal, el programa concreto del marcapasos.
La especificación del problema se realizó en términos de grafos temporizados. Como resultado se obtuvieron distintos modelos que respondían a distintos modos del marcapasos. Los modos del marcapasos indican si se estimula el corazón, y en caso afirmativo si el estímulo es auricular o ventricular. El modelo realizado describe el comportamiento del programa en todos los modos, salvo los que actúan sobre la cámara auricular. Estos modelos comprendían el comportamiento de todos los modos, salvo aquellos que involucraban a la cámara auricular. Los mismos fueron validados con integrantes de la empresa CCC.
Siguiendo este enfoque se formularon y probaron propiedades sobre el modelo. Podemos distinguir dos tipos de propiedades: la correspondientes al modelo propiamente dicho, y las que corresponden al objeto modelado. La más importante de las propiedades del modelo es la de buena temporización, que muestra la consistencia interna del mismo. La principal propiedad verificada del objeto modelado es la seguridad del sistema, condensada en la siguiente frase: el corazón realiza late, ya sea en forma natural o estimulado artificialmente, a la velocidad deseada. Estas propiedades de seguridad se expresan como fórmulas de la lógica temporal TCTL.
Esta etapa proporcionó una primera aproximación formal al problema y favoreció el aprendizaje del código real del programa. Formalmente, dio lugar a la concreción de las actividades 1 y 2 del proyecto.
El análisis del programa del marcapasos se puede realizar en un marco lógico desde dos estrategias, conocidas como superficial y profunda. En el primer caso, se traduce el código al lenguaje propio del marco lógico; en el segundo, se construye un intérprete del lenguaje dentro del mismo marco.
Al contrario que la estrategia profunda, la estrategia superficial es alcanzable con un conocimiento de usuario del marco lógico. En consecuencia, para poder comparar distintos marcos, ensayamos este enfoque. Se realizaron pruebas simples con PVS, Coq, e Isabelle, siguiendo la literatura. La misma se centra en la descripción detallada de lenguajes orientados a objetos [Hui01, Boe03]. En cambio, los problemas referidos a lenguajes imperativos empleados en sistemas críticos no son suficientemente generales, debido a una serie de características específicas: granularidad de los tipos de datos, uso de relojes, gestión de la memoria. En consecuencia, nos resultaba necesario incorporar algunos de estos elementos en soluciones públicas, o construír una solución desde cero. Ambas acciones exigían un costo de programación elevado, lo que llevó a postergar esta estrategia en favor del tercer punto que referimos más adelante.
La comparación entre las distintas herramientas no ha podido realizarse en forma exitosa. Más allá de las caracterizaciones obvias que surgen del uso inmediato de las mismas, no pudimos establecer un marco común a todas las herramientas. Los criterios a tomar en cuenta requieren un mayor análisis que el realizado hasta hoy. Sin embargo, podemos destacar que entre ellos se encuentran: lógica implementada, tamaño de las pruebas, portabilidad y modularidad del marco.
El análisis estático es una estrategia que intenta obtener información acerca de las ejecuciones de un programa a partir de un conjunto de simulaciones simbólicas del mismo. Este acercamiento fue de interés a partir del aprendizaje de las herramientas Bandera y ESC/Java. Se desconocía el mismo, y se destinó tiempo a estudiar las posibles aplicaciones del enfoque.
Con este enfoque nos centramos en un problema acotado: el valor de las variables del programa. En el caso en que se emplean dispositivos electrónicos, se incorpora al problema la noción de estabilidad: un elemento del microcontrolador está estable cuando no está sufriendo cambios a nivel físico. En nuestro código ciertas variables se implementan como dispositivos electrónicos, y por tanto pasibles de estar inestables. Al asignarles valores a estas variables, pasan por un momento de inestabilidad durante el cual su valor no está bien definido. Nos preocupamos entonces de la siguiente propiedad: al usar variables en el programa, las mismas se encuentran estables. A partir de esta propiedad se desarrolló un modelo, siguiendo las pautas del análisis de flujo de datos, que permitiría verificarla en el código del marcapasos.
La implementación de esta estrategia se realizó para un lenguaje muy simple, con estructuras de control habituales y tiempos de ejecución explícitos . En caso que la propiedad no se cumpla, se propone, en forma automática, acciones posibles para paliar la situación. Debido a que los programas a estudiar son de caracter crítico, la decisión última de los cambios a realizar es dejada en manos del programador experto. La extensión de esta propuesta a otros lenguajes parece razonablemente alcanzable. A la fecha aún no se ha comenzado con esa posibilidad.
El esquema de trabajo propone la siguiente línea de acción:
La última observación correspondiente a este punto es que en los últimos años se ha intentado unificar las propuestas de análisis estático y verificación de modelos[Sch98, Cou99]. Entre otros beneficios, este acercamiento permitiría eliminar la construcción de un nuevo programa por cada propiedad que se desea verificar. Sin embargo, este acercamiento solo ha afectado a los sistemas que no tienen características de tiempo real. Dirigimos nuestra atención a la búsqueda de un marco unificador entre análisis estático y verificación de modelos que comprenda los sistemas de tiempo real. Formalmente, este punto dio lugar a la concreción de las actividades 3, 4 y 6 del proyecto.
Los siguientes resultados concretos han sido obtenidos a lo largo del proyecto:
El proyecto ha dejado distintas líneas de estudio e implementación.
El último punto propone extender la relación estudiada entre verificación de modelos finitos y análisis estático. En caso contrario, los sistemas de tiempo real quedarían excluídos de este acercamiento dada la infinitud de su universo de discurso.
| ----------------------- | ----------------------- |
| Responsable | Tutor |