Proyecto : Verificación formal automatizada de un marcapasos
Detalles de la Investigación
A.- Resumen de la investigación
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.

Detalles de la Investigación
B.‑ Fundamentación y antecedentes.
Resumen
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, causando una considerable pérdida de tiempo al equipo de programación, o dañando considerablemente la imagen de la empresa si el programa ya está siendo comercializado. El costo de estos errores es considerado el mayor en todas las etapas del proceso de desarrollo de sistemas informáticos.

Esta exigencia de cero defecto hace que ciertas normas internacionales de calidad impongan la verificación de código como etapa obligatoria (y no optativa) del desarrollo de software. Por otra parte, a lo largo de estos años 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 que se plantea hoy a los investigadores del Grupo de Métodos Formales del InCo es continuar el desarrollo de dichas herramientas así como experimentar e integrar las técnicas propuestas, buscando dar respuesta a las necesidades actuales y futuras de la industria local.

En Uruguay se desarrollan hoy cierto número de aplicaciones críticas. Un ejemplo de éstas es el código de microcontroladores utilizados en marcapasos. En este contexto, existe un interés explícito por parte de la empresa CCC (Centro de Construcción de Cardioestimuladores del Uruguay) en aplicar técnicas formales para el estudio de la corrección de dicho código. Como gran parte de las aplicaciones críticas, los microcontroladores empleados en los marcapasos pertenecen a una familia de programas informáticos llamados programas reactivos. Estos programas iteran en un ciclo normalmente infinito de estímulo-respuesta en relación al medio. La certificación matemática de la correctitud de este tipo de sistemas informáticos incorporando a la misma herramientas automáticas constituye el núcleo alrededor del cual se comprende el presente proyecto.
Estado actual del conocimiento
En la actualidad, el método más usado en la industria de la programación para validar un sistema informático consiste en realizar simulaciones sobre una batería de casos de prueba considerados razonablemente representativos de las ejecuciones posibles del programa [Ghezzi 91]. Este método no garantiza una confianza absoluta en el programa, dado que en la mayoría de los casos se trata de una verificación incompleta de todas las situaciones posibles que se podrían encontrar. Los errores lógicos no detectados mediante este procedimiento que aparecen en los controladores de hardware, protocolos de comunicación y sistemas de tiempo real se han convertido en un problema de primer orden para la comunidad académica e industrial vinculada a la producción.

Durante los últimos años la comunidad académica ha propuesto distintos enfoques alternativos para garantizar formalmente la corrección de un sistema informático. Todas estas técnicas comparten el uso de lenguajes formales, en los cuales es posible describir con precisión las propiedades que se esperan del programa. Se llama especificación a esta descripción rigurosa de las propiedades de un programa. En este marco, un sistema informático es correcto si satisface su especificación.

Es necesario notar que la descripción del sistema informático no es directamente el código del programa. Es una aspiración de la investigación actual en este campo, y de este proyecto en particular, encontrar mecanismos que permitan transitar desde este lenguaje de definición del sistema al lenguaje de programación en que el sistema se encuentra programado efectivamente. En esta dirección es que se encuentra este proyecto vinculado a las actividades actuales del GMF.
Verificación de modelos
El método de validación de sistemas informáticos conocido como verificación de modelos (“model checking”) [Henzinger 92, Alur 94, Alur 95] se basa en la verificación exhaustiva de todas las posibles ejecuciones de un sistema informático. Desde esta óptica, un programa es considerado correcto cuando se prueba que no hay ninguna ejecución posible que viole su especificación.

En esta perspectiva coexisten dos lenguajes formales (que eventualmente pueden coincidir): el de definición del sistema, en el cuál se expresa el sistema informático a validar, y el de definición de la especificación. Un procedimiento eficiente determina automáticamente si la especificación es satisfecha por el sistema. Esta técnica ha sido usada con éxito para detectar errores sutiles en distintos sistemas, en particular en protocolos de comunicaciones. 

Durante los últimos años el tamaño de los sistemas informáticos que pueden ser verificados de esta manera se ha incrementado considerablemente. Esto ha sido consecuencia del desarrollo de nuevas técnicas de recorrido del espacio de búsqueda, como por ejemplo la verificación simbólica de modelos y la verificación al vuelo (“on the fly”). Entre las herramientas que implementan alguna de estas técnicas se destacan Kronos (Laboratorio VERIMAG) [Daws 96], Uppaal (Universidades de Uppsala y Aalsborg) [Uppaal], y HyTech (Universidad de Berkeley) [Hytech], entre otras.
Caso de estudio: microcontrolador del marcapasos
El microcontrolador elegido para este proyecto es un caso especialmente interesante para el empleo intensivo de técnicas formales de verificación. Como atributos que favorecen la realización de este estudio se pueden señalar:
•	pequeñez del código. La misma tiene dos buenas cualidades: el tiempo de desarrollo de la especificación del sistema se puede acotar en tiempos razonables, y se habilita a la experimentación con herramientas que estando en su desarrollo inicial aún no son capaces de tratar problemas de gran porte.
•	es un sistema crítico. Su empleo en medicina exige un grado de confianza que se alcanza mediante el uso de técnicas formales. La exigencia del estudio exacto del problema lleva a tratar exhaustivamente los detalles del código, generando así un mayor aprendizaje en las potencialidades de los métodos formales.
•	especificación clara. Propiedades del microcontrolador que miembros del equipor de desarrollo de CCC están interesados en que sean verificadas son, por ejemplo:
•	se intentará hacer una comunicación al menos cada 2 segundos.
•	luego de un evento ventricular (sensado o estimulado) no se sensará ningún evento durante el tiempo programado para el refractario.
•	si se sensa una señal a una frecuencia mayor que 11 Hz el marcapasos se comportará como si no sensara, y se irá a la frecuencia base programada.
•	inserción del proyecto en el GMF. El mismo se desarrollará armónicamente con los esfuerzos de certificación de código desde otras ópticas, permitiendo obtener un cruzamiento entre los distintos trabajos que se enriquecerán mutuamente.
•	vínculos con CCC. La relación del GMF con la empresa CCC se ha llevado adelante en forma fluida hasta la fecha, y no existen indicios aparentes de que la misma vaya a cambiar. Esto nos habilita a mantener un diálogo amplio con el equipo de desarrollo del código que se desea verificar.
Relevancia del tema propuesto
Se espera como resultado del proyecto una metodología para la validación de programas que integre técnicas formales ya disponibles, y que pueda ser aplicada a problemas de corte real de la industria uruguaya y de la región. El proyecto apuntalará la formación de un equipo experimentado en el uso de técnicas formales, que pueda vincularse con empresas interesadas en técnicas de verificación formal de código crítico.

La relevancia de la investigación a desarrollar en este proyecto puede analizarse desde diferentes perspectivas, todas ellas enmarcadas en el trabajo del GMF:
1.	para CCC significa recibir asesoramiento en lo que hace al área de verificación. Esto es importante, considerando que la complejidad de los sistemas informáticos tiende a incrementarse continuamente. En consecuencia, somos optimistas en cuanto a las repercusiones que un proyecto exitoso de estas características pueda tener en la comunidad industrial local.
2.	para los investigadores es una oportunidad de experimentar fuera del ambiente académico las técnicas de verificación que se han desarrollado a lo largo de estos años. Esto permitirá comprender sus limitaciones y proponer futuras extensiones o mejoras, además de clarificar la posibilidad de usar en forma integrada distintas herramientas.
3.	se espera que el presente proyecto influya en la formación de estudiantes de grado y posgrado con un nuevo perfil.
4.	se espera que los resultados obtenidos por esta investigación darán lugar a la producción de artículos científicos en las siguientes temáticas: verificación automática de sistemas reactivos, integración de herramientas automáticas, semántica de los leguajes de programación.
Antecedentes del docente responsable
Luis Sierra, docente responsable de esta propuesta, es integrante del Grupo de Métodos Formales del Instituto de Computación. Dentro de sus tareas docentes ha participado en cursos de Programación, Lógica, y Verificación de Sistemas de Tiempo Real. Otras actividades cercanas al problema de la verificación de sistemas reactivos ha sido la supervisión de trabajos de grado vinculados al mismo [Arcia 99, Bernasconi 97], y la especificación y validación parcial de un protocolo de comunicaciones [SierraB 98]. Su tesis de maestría consistió en un nuevo enfoque acerca de los sistemas distribuidos basados en una noción abstracta de localidad [SierraA 98], que obtuvo el quinto lugar en el concurso de Tesis de Maestría organizado por el CLEI y la UNESCO. Actualmente, se encuentra realizando un trabajo comparativo entre distintas herramientas automáticas de verificación en coordinación con investigadores de la Ecole Normal Superieure de Cachan, París. En lo que respecta a su formación, se encuentra realizando su Doctorado en Informática en temas vinculados a la búsqueda de una metodología que armonice el uso de distintos métodos formales para la validación del sistemas informáticos.
C.‑ Objetivos generales y específicos.
El objetivo general de la investigación en que se enmarca este proyecto consiste en la elaboración de una nueva metodología de validación de software empleando técnicas formales, aplicada a un problema concreto e interesante de la industria electrónica nacional.

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 las siguientes perspectivas:
a)	expresibilidad de las propiedades del sistema
b)	eficiencia de las distintas herramientas
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.
1)	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:
a)	ejemplos que muestren la incorrectitud del software
b)	estrategias para reparar el sistema
c)	un nuevo software correcto
D.- Especificación de las preguntas que busca responder el proyecto.
El presente proyecto aspira contestar preguntas a dos niveles: un nivel académico, y un nivel de relacionamiento con el medio. Dada las características del proyecto, dichos niveles aparecen poco diferenciados en algunas casos.
•	validar la especificación y la implementación del código para los microcontroladores empleados en la producción de marcapasos.
•	estudiar la posibilidad de extender el método de verificación de modelos más allá de la especificación del sistema, comprendiendo especialmente la verificación del código.
•	estudiar el uso conjunto de distintas herramientas automáticas para la verificación de sistemas.
•	explotar el empleo de métodos formales de verificación de corte académica en el ambiente de la industria local. En la actualidad, este empleo es habitual para las industrias del primer mundo vinculadas a la producción de sistemas informáticos de gran porte o de características críticas.
E.‑ Estrategia de investigación.
La estrategia a llevar adelante durante este proyecto tendrá presenta las siguientes características:
•	el responsable del proyecto se encontrará realizando su doctorado en Informática.
•	se continuarán y profundizarán los contactos con investigadores extranjeros de laboratorios de primer nivel.
•	el éxito de este proyecto tendrá relevancia en el mercado de la industria electrónica.

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:
•	estudio del sistema del marcapasos
•	acercamientos al problema desde el punto de vista de la verificación de modelos
•	uso intensivo de herramientas automáticas
•	desarrollo de herramientas que faciliten la integración de las herramientas citadas anteriormente
•	presentación en la comunidad académica (publicaciones, conferencias, etc.) y no académica de los avances de la investigación
F.‑ Actividades específicas.
Las actividades específicas de este proyecto serán las siguientes:
1)	Análisis del microcontrolador. Familiarización con el problema.
a)	Estudio del problema concreto, realizado de acuerdo a las técnicas habituales para el relevamiento y análisis de problemas.
2)	Elaboración de una especificación formal del microcontrolador, por medio de:
a)	construcción de modelos
b)	verificación de propiedades
3)	Análisis del código
a)	construcción de un modelo a partir del código
b)	verificación de propiedades
4)	Comparación y acercamiento entre los ítems 2 y 3.
5)	Análisis comparativo de las herramientas utilizadas.
a)	en cuanto a la potencia como lenguaje de especificación
b)	en cuanto a las propiedades estudiadas
6)	Caracterización de la metodología empleada, considerando
a)	técnicas de prueba
b)	herramientas utilizadas
c)	validación del microcontrolador
7)	Elaboración de documentación.
a)	Presentación de resultados intermedios y finales en ámbitos científicos y técnicos apropiados
b)	Informes relevantes al buen relacionamiento con la empresa CCC
c)	Informes relevantes a fin de la supervisión y evaluación del desarrollo del proyecto.
G.‑ Materiales y métodos.
El trabajo se realizará sobre workstations Sun Sparc con 50 M de memoria. El uso de máquinas de porte es inherente al uso de herramientas de verificación automática. Las instalaciones en que se llevará adelante el proyecto serán las correspondientes a las del GMF.
H.‑ Cronogramas de ejecución.
La numeración empleada es la correspondiente a l ítem F-Actividades específicas.
Cronograma correspondiente al primer año
	I	II	III	IV	V	VI	VII	VIII	IX	X	XI	XII	
1a													
2a													
2b													
3a													
3b													
4													
5a													
5b													
6a													
6b													
6c													
7a													
7b													
7c													
Cronograma correspondiente al segundo año

	I	II	III	IV	V	VI	VII	VIII	IX	X	XI	XII	
1a													
2a													
2b													
3a													
3b													
4													
5a													
5b													
6a													
6b													
6c													
7a													
7b													
7c													
I.- Describa el personal asignado al proyecto así como el personal a contratar. 
Se solicita una compensación salarial de acuerdo a los criterios de la Universidad de la República para el Responsable del Proyecto, Luis Sierra. Dicho complemento salarial es por los dos años del proyecto, en un cargo de Asistente (Grado 2), 40 hs semanales.
J.‑ Resultados esperados.
Los resultados que se esperan de este proyecto son:
1)	Compación a través del caso de estudio del marcapasos 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
a)	expresividad del lenguaje de especificación: por ejemplo, identificar que clase de problemas resulta más fácil describir en cada una.
b)	eficiencia de las distintas herramientas.
c)	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 confortable, y en el mejor de los casos integrado, de distintas herramientas de verificación.
K.-  Estrategias de difusión.
Se espera poder publicar trabajos en conferencias y revistas arbitradas de relevancia en la temática correspondiente.
En caso de implementarse herramientas de caracter general para integrar las distintas herramientas a analizar, se las hará disponibles públicamente para un mejor desarrollo de la verificación automática por parte de la colectividad académica.
Los resultados concernientes a la validación del marcapasos se difundirán en conjunto con la empresa CCC en la forma y modo en que se acuerde.
L.-  Impacto y/o beneficios de los resultados.
Dentro de los impactos que esperamos como resultado de este proyecto mencionamos:
•	una valoración positiva en el entorno local del problema de la verificación formal y del uso de los métodos formales, tanto en el ámbito industrial como en el académico,
•	un estrechamiento de los vínculos del GMF con las industrias que en Uruguay generan sistemas informáticos de características críticas, pasibles de ser tratados formalmente,
•	la conformación en la región de un grupo regional, que comprenda centros de investigación de Argentina y Brasil, interesado en continuar investigaciones en el área, dentro del cual la Universidad juegue un papel relevante, y
•	obtener resultados que permitan continuar nuestras relaciones con centros de investigación internacionales de primer nivel con un mayor reconocimiento a nuestro trabajo.

M.‑ Referencias bibliográficas.

[Alur 94] Rajeev Alur and David Dill. “A theory of timed automata”.En Theoretical Computer Science, 1994.

[Alur 95] Rajeev Alur, Costas Courcoubetis, N. Halbwachs, Thomas A.Henzinger, P.-H.Ho,
  Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, y Sergio Yovine. “The algorithmic analysis of hybrid systems”.En Theoretical Computer Science, 138:3--34, 1995.

 [Arcia 99] Andrea Arcia y Marcos González. “Estudio de sistemas de tiempo real en equipos biomédicos”. Trabajo de grado de Ingeniería en Computación, InCo, Universidad de la República, Uruguay, Marzo 1999.

[Bernasconi 97] Renzo Bernasconi. “Modelización y verificación del caso de estudio Production Cell”. Trabajo de grado de Ingeniería en Computación, InCo, Universidad de la República, Uruguay, Julio 1997.

[Daws 96] Conrado Daws, Alfredo Olivero, Stavros Tripakis, y Sergio Yovine. “The tool KRONOS”. En Hybrid Systems III, Verification and Control, LNCS 1066, 1996.

[Ghezzi  91] Carlo Ghezzi, Mehdi Jazayeri y Dino Mandrioli. “Fundamentals of Software Engineering”. Prentice Hall, 1991.

[Henzinger 92] Thomas A. Henzinger, Xavier Nicollin, Joseph Sifakis, y Sergio Yovine. “Symbolic model checking for real-time systems”. En Proceedings of the 7th IEEE Symposium Logic in Computer Science, Junio 1992.

[Hytech] “HyTech: The HYbrid TECHnology Tool” Página web: http://www-cad.eecs.berkeley.edu/~tah/HyTech/, Universidad de Berkeley.

[SierraA 98] Luis Sierra. "Automatic Verification of Hybrid Systems: An Audio Control Protocol". En Conference Proceedings from the International Conference of the Chilean Computer Science Society (SCCC'98).

[SierraB 98] Luis Sierra. "Retrieving Spatial Distribution from Semantics". Technical report 9805,  INCO.

[Uppaal] “UPPAAL - Validation and Verification Tools for Real-Time Systems” Página web: http://www.docs.uu.se/docs/rtmv/uppaal/index.shtml, Universidad de Uppsala.