Especificación y verificación de marcapasos : un método de modelado utilizando grafos temporizados

Loading...
Thumbnail Image
Date
2015
Authors
Damonte Callorda, Pablo Gabriel
Publisher
Universidad ORT Uruguay
DOI
ISSN
ISBN
Abstract
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.
En
Thesis note
Desarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingeniería
Thesis degree name
Master en Ingeniería
66 p. il., diagrs
Notes
Incluye bibliografía.
Incluye archivos complementarios.
Subject
PROYECTOS-MI, MÉTODOS FORMALES, MARCAPASOS CARDÍACOS
Type
Trabajo final de carrera
Access the full text
Citation
Damonte Callorda, P. G. (2015). Especificación y verificación de marcapasos: un método de modelado utilizando grafos temporizados (Desarrollo de Tesis). Universidad ORT Uruguay, Facultad de Ingeniería. Recuperado de https://rad.ort.edu.uy/handle/20.500.11968/3169
Rights license