En este informe se hace referencia al punto F.- Actividades específicas de la propuesta planteada originalmente en el programa de Iniciación a la Investigación presentada en 1999. Se agrega una sección acerca de actividades laterales al proyecto impulsadas desde el mismo, con la perspectiva de obtener un mayor impacto.
En un documento anexo se describe la situación de los gastos realizados en el correr del semestre, y la situación esperada del resto de los fondos.
En un segundo anexo se trascriben fragmentos de la propuesta originaria de estas actividades.
El estudio del microcontrolador se ha realizado con dos estrategias: el estudio del código, y el diálogo con los desarrolladores del mismo.
Al estudiar el código se ha profundizado en el conocimiento de dialectos del lenguaje C destinados específicamente a la programación de sistemas embebidos de tiempo real. Se han estudiado someramente otros lenguajes que presentan características similares. En particular, he centrado mi atención en dos propuestas alternativas sobre este problema, como son los sistemas operativos de tiempo real y las extensiones específicas de lenguajes de programación y especificación para trabajar con sistemas embebidos.
Del diálogo con los desarrolladores del microprocesador se tomaron en consideración decisiones de diseño y requerimientos de seguridad. Ciertas decisiones de programación y el modelo de desarrollo de sus códigos, que responden a problemas particulares de su entorno, han emergido de estos diálogos. Las más relevantes a los fines de este proyecto son: a nivel de implantación, la revisión permanente de los códigos generados por los compiladores, y la perspectiva próxima de un aumento en la disponibilidad de recursos computacionales de los microprocesadores empleados; a nivel de desarrollo y aceptación del producto, el interés en la obtención de certificaciones de calidad de sus códigos. Las especificaciones de seguridad que debe tener el código fueron tomadas de estas conversaciones y de la documentación que nos fue brindada.
La estrategia habitual de verificación por casos particulares (testing), no ha sido empleada, debido al supuesto que rige esta actividad: la afirmación de Edsger Dijkstra de que la prueba por casos sirve para encontrar errores en los programas, pero no para probar la corrección de los mismos. Adhiriéndonos a este pensamiento, y siendo preocupación central del Grupo de Métodos Formales el desarrollo de programas correctos, esta estrategia no sería adecuada a los fines del presente proyecto.
La especificación formal del microprocesador se realizó empleando la herramienta Kronos. La misma provee un lenguaje de especificación de sistemas de tiempo real, un lenguaje de especificacion de propiedades, y un motor computacional que prueba la validez o invalidez de cierta propiedad en un sistema. Kronos pertenece a la familia de herramientas conocidas como verificadores de modelos (model checkers).
La especificación del sistema y la prueba de algunas propiedades de seguridad fueron realizadas y comunicadas a los desarrolladores del software estudiado. Como resultado de las mismas, se aclaró la comprensión del problema y se reafirmaron los vínculos con los desarrolladores.
El estudio del código es una de las actividades que se están realizando en este momento. La estrategia original consistía en emplear una técnica conocida como ubicación superficial (shallow embedding) del programa en un ambiente lógico (logical framework), en el cual probar deductivamente las propiedades de interés. Como forma alternativa a este acercamiento, se propuso la construcción de un modelo de grafos temporizados a partir del código y la demostración de que este modelo y la especificación mantenían cierta relación de equivalencia. El análisis estático, estrategia conocida para estudiar códigos, apareció como mecanismo natural para emprender esta tarea. La adopción de herramientas específicas de esta estrategia, y el estudio con mayor profundidad de la misma, constituyen actividades actualmente en realización.
Los avances concretos en el análisis del código han abarcado: la delimitación del caso de estudio a un subconjunto bien definido del código, y la construcción de un modelo abstracto de parte de dicho subconjunto. Hay que comprender que el microcontrolador comprende nueve modos diferentes de operación: los mismos interactúan débilmente, así que es factible su estudio por separado. El caso de estudio fue delimitado a tres de dichos modos. El modelo abstracto se ha elaborado sobre dos de estos tres modos, pero aún no se ha probado la corrección de dicha abstracción.
Está pendiente.
Existen dos niveles distintos de comparación: a nivel de clases (verificadores de modelos y ambientes lógicos con análisis estático), y a nivel de herramientas propiamente dichas (Kronos, HyTech, UppAal, Spin, RTSpin, Coq, Isabelle, PSV, Bandera). Inicialmente, nuestra preocupación se centraba en la comparación a nivel de clases. Hoy día, el proyecto se ha centrado en la verificación del código de tal forma que hace inviable dicha comparación. Nos encontramos desarrollando una metodología híbrida, sin haber acabado un análisis comparativo. No considero esto como una falla en el desarrollo, sino como la constatación, a partir de la propia experiencia y de la literatura científica hoy preponderante, de la profunda imbricación entre los distintos enfoques. En consecuencia, este punto está aún pendiente, y quizá deba reformularse.
En desarrollo.
Se han presentado resultados parciales en conferencias locales, seminarios internos en el InCo, la ENS de Cachan, y el INRIA-Rocquencourt, y charlas con los desarrolladores del producto.
Como actividad docente he impulsado algunas actividades que cooperan en la dirección del proyecto. Las mismas incluyen: