Título:
Hacia una especificación formal de un microcontrolador usado en marcapasos
Otros títulos:
Coordinador:
Director:
Compilador:
Autor:
Luna, Carlos
Echenique, Paula
Sierra Abbate, Luis Ricardo
Echenique, Paula
Sierra Abbate, Luis Ricardo
Tutor:
Tipo de documento:
Reporte técnico
Editor:
Palabras clave:
Microcontroladores (PICs)
Especificaciones Formales
Coq
Especificaciones Formales
Coq
Descriptores:
Año de publicación:
2008
Contenido:
Resumen:
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 este artículo 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.
Descripción:
Editorial:
UR. FI – INCO.
EN:
Reportes Técnicos 08-09
Financiadores:
Citación:
LUNA, C., ECHENIQUE, P., SIERRA ABBATE, L. "Hacia una especificación formal de un microcontrolador usado en marcapasos". Reportes Técnicos 08-09. UR. FI – INCO, 2008.
Citación:
metadata.cc.license.name:
Documento del Gobiberno:
URI:
http://hdl.handle.net/20.500.12008/3561
ISBN:
e-ISBN:
ISSN:
0797-6410
ISMN:
Otros identificadores:
Título Obtenido:
Facultad o Servicio que otorga el Título:
Licencia:
Licencia Creative Commons Atribución – No Comercial – Sin Derivadas (CC BY-NC-ND 4.0)
Cobertura geográfica:
Cobertura temporal:
metadata.dc.relation.IsVersionOf:
Clasificación:
Es versión de:
Colecciones:
| Ficheros | Descripción | Tamaño | Formato | ||
|---|---|---|---|---|---|
| TR0809.pdf | — | 117.28 KB | Adobe PDF |