Título: Especificación Formal de un Microcontrolador usado en Marcapasos

Marco de Trabajo: Maestría

Área de desarrollo: Métodos Formales

Autor: Paula Echenique

Contacto: paula.echeniquevinas@gmail.com

Día: JUEVES

Hora: 14:15

Palabras Claves: Microcontroladores, Métodos Formales

Resumen:
Tutores: Carlos Luna y Luis Sierra| Un microcontrolador es un circuito integrado que contempla las funcionalidades de un computador. Los avances tecnológicos de las últimas décadas han permitido que los microcontroladores se usen hoy en diferentes ámbitos; por ejemplo, en dispositivos de comunicación como los celulares o de control médico como los marcapasos. En este trabajo analizamos una familia de microcontroladores programables llamada PIC. El microprocesador cuenta con un programa modificable, que lo convierte, esencialmente, en una computadora de uso general, pequeña, barata, y versátil. Nuestro interés se centra en la verificación de programas críticos desarrollados en este entorno. En particular, nuestro objetivo final es el estudio de programas para dispositivos biomédicos implantables. En esta charla presentamos la formalización de un PIC usando máquinas de estados. Especificamos el comportamiento de las instrucciones de la máquina y certificamos, usando el asistente de pruebas Coq, el funcionamiento de la misma, expresado a través de una semántica operacional. |