RESERVAS DE VERANO:
Las Bibliotecas permanecerán cerradas desde el 30/12/2019 hasta el 19/01/2020 inclusive.
Por información sobre reservas de verano debe ingresar al sistema.

Detalles de la obra

Título:
Especificación y verificación de marcapasos
Subtítulo:
un método de modelado utilizando grafos temporizados
Autor(es):
Damonte Callorda, Pablo Gabriel
Pie de imprenta:
Montevideo: Universidad ORT Uruguay, 2015
Descripción física:
66 p. il., diagrs. En línea
Nota de tesis:
Desarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingeniería. Montevideo, 2015. Calificación: 95/100
Título obtenido:
Entregado como requisito para la obtención del título de Master en Ingeniería
Tutor:
Álvaro Daniel Tasistro Souto
Tribunal:
Cristina Roxana Cornes Boquete; Sergio Fabián Yovine Seijas
Resumen:
Los sistemas de tiempo real, en general, requieren que su funcionamiento carezca de fallas. En el caso de los controladores de marcapasos, esto resulta de vital importancia. En el marco del desafío propuesto por el fabricante de marcapasos Boston Scientific, en este trabajo se plantea una metodología lo más didáctica posible que permita obtener una correcta especificación de los sistemas y detectar fallas en su diseño en las etapas más tempranas. Para que un sistema no falle, es necesario tener certeza de que su especificación es correcta, para luego continuar con su diseño y, finalmente, con su implementación. Luego de analizar diversos trabajos que intentan resolver este problema, se propone una notación gráfica, extensión de grafos temporizados con facilidades de abstracción, para la representación de los diferentes modos de operación de un marcapasos y se presenta una metodología con un enfoque pedagógico. Se propone, entonces, un modelo de corazón que permite reflejar diferentes anomalías en su funcionamiento real, analizándose su interacción con los diferentes modos de operación de marcapasos modelados. Los modelos se representan mediante el sistema UPPAAL. Posteriormente, usando el chequeador de modelos de UPPAAL se verifica un número de propiedades consideradas básicas para el correcto funcionamiento de los modelos: si el sistema no se bloquea, si no se detectan pulsos en los períodos refractarios, si no transcurre más de un tiempo prefijado entre dos estimulaciones o pulsos intrínsecos consecutivos. Finalmente se considera la posibilidad de continuar la línea de investigación y llegar a la generación del código del marcapasos o ampliar la línea de investigación y generalizar el método propuesto para contemplar otro tipo de dispositivos médicos implantables.
Notas:
Incluye archivos complementarios.
Referencias bibliográficas:
Incluye bibliografía.
Idioma:
Español
Tipo de material:
[Trabajo Final de Carrera]
Ubicación física:
Disponible en línea

Archivos asociados:

Archivo Tamaño Formato
Desarrollo de Tesis 1.25MB application/pdf
Informe del corrector 26kB application/pdf