Abstract: La verificacion del software de marcapasos cardıacos implantables es de vital importancia
debido a que fallos en el firmware de marcapasos y desfibriladores implantables
causaron el retiro del 41 % de estos por medidas de seguridad para
el paciente entre los anos 1990 y 2000. Es necesario establecer una metodologıa
formal que permita verificar el software de los marcapasos, ya que un 70 % de
los pacientes que padecen arritmias cardıacas en Venezuela necesitan tratamiento
con un marcapasos temporal o implantable segun informes recientes del anuario
de epidemiologıa y mortalidad. Se construyo un sistema virtual de evaluacion de
marcapasos, implementado usando automatas temporizados de estados, capaz de
emular el funcionamiento de los tejidos del corazon y su reaccion ante un impulso
electrico generado por un marcapasos cardıaco DDD. Se incorporo en el modelo
del corazon virtual (VHM) las caracterısticas de respuesta de la senal electrica del
corazon humano al percibir un estımulo anticipado capaz de modificar la velocidad
de conduccion y los periodos refractarios relativos de los tejidos. Probando
que el modelo del marcapasos empleado es el correcto y contiene las condiciones
necesarias para aplicar una estimulacion o inhibir la misma segun la necesidad del
paciente. Ademas de proveer un sistema en lazo cerrado del VHM y del marcapasos
cardıaco DDD modelado que permite evaluar el software del dispositivo medico.