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

Simple item page
dc.contributor.advisorTasistro Souto, Álvaro Danieles
dc.contributor.tribunalCornes Boquete, Cristina Roxanaes
dc.contributor.tribunalYovine Seijas, Sergio Fabiánes
dc.creatorDamonte Callorda, Pablo Gabriel
dc.date.accessioned2017-06-14T14:43:27Z
dc.date.available2017-06-14T14:43:27Z
dc.date.issued2015es
dc.descriptionIncluye bibliografía.es
dc.descriptionIncluye archivos complementarios.es
dc.description.abstractLos 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.es
dc.format.extent66 p. il., diagrses
dc.identifier.citationDamonte 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/3169es
dc.identifier.urihttp://hdl.handle.net/20.500.11968/3169
dc.languageEspañoles
dc.publisherUniversidad ORT Uruguayes
dc.relation.otherhttps://bibliotecas.ort.edu.uy/bibid/81235es
dc.subjectPROYECTOS-MIes
dc.subjectMÉTODOS FORMALESes
dc.subjectMARCAPASOS CARDÍACOSes
dc.titleEspecificación y verificación de marcapasoses
dc.title.subtitleun método de modelado utilizando grafos temporizadoses
dc.typeTrabajo final de carreraes
ort.thesis.careerFI - Master en Ingeniería - MIes
ort.thesis.degreegrantorFacultad de Ingenieríaes
ort.thesis.degreelevelMasteres
ort.thesis.degreenameMaster en Ingenieríaes
ort.thesis.degreetypeDesarrollo de Tesises
ort.thesis.noteDesarrollo de Tesis (Master). Universidad ORT Uruguay, Facultad de Ingenieríaes
Files
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
Name:
Material completo.pdf
Size:
1.19 MB
Format:
Adobe Portable Document Format
Description:
description
Download
Collections
Trabajos finales de carrera de postgrado