Especificación y verificación de marcapasos : un método de modelado utilizando grafos temporizados [Trabajo Final de Carrera]

Autor/es: Damonte Callorda, Pablo GabrielDatos de publicación: Montevideo: Universidad ORT Uruguay, 2015Descripción física: 66 p. il., diagrs EN LÍNEANota de tesis: Desarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingeniería. Montevideo, 2015. Calificación: 95/100 Título obtenido: Master en Ingeniería
Tutor: Tasistro Souto, Álvaro Daniel
Tribunal: Cornes Boquete, Cristina Roxana | Yovine Seijas, Sergio Fabián
Tema(s): MARCAPASOS CARDÍACOS | MÉTODOS FORMALES | PROYECTOS-MIRecursos en línea: Material completo | Informe del corrector (Requiere ingresar al sistema para acceder al archivo solicitado) 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.
Valoración
    Valoración media: 0.0 (0 votos)
Existencias
Tipo de ítem Biblioteca de origen Signatura topográfica Estado Fecha de vencimiento Código de barras
Trabajo Final de Carrera Trabajo Final de Carrera Centro Disponible en línea No para préstamo

Incluye archivos complementarios.

Incluye bibliografía.

Tasistro Souto, Álvaro Daniel Cornes Boquete, Cristina Roxana Yovine Seijas, Sergio Fabián

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.

Español

No hay comentarios en este titulo.

para colocar un comentario.