000005302 001__ 5302 000005302 005__ 20150325135749.0 000005302 037__ $$aTAZ-TFM-2010-075 000005302 041__ $$aspa 000005302 1001_ $$aRequeno Jarabo, José Ignacio 000005302 24500 $$aAnálisis filogenético mediante lógica temporal y model checking 000005302 260__ $$aZaragoza$$bUniversidad de Zaragoza$$c2010 000005302 506__ $$aby-nc-sa$$bCreative Commons$$c3.0$$uhttp://creativecommons.org/licenses/by-nc-sa/3.0/ 000005302 500__ $$aRealizado bajo la tutela de una beca de iniciación a la investigación del I3A 000005302 520__ $$aEl análisis filogenético es la rama de la bioinformática que se encarga de estudiar la clasificación de un conjunto de especies distintas en función de su relación de proximidad evolutiva. La metodología de trabajo que sigue actualmente es muy “ad-hoc”; es decir, cuando especificamos una nueva propiedad biológica o añadimos otra especie al modelo necesitamos reimplementar el algoritmo de verificación para que considere los nuevos datos. Para solucionarlo, nuestra aproximación trata de sistematizar el método de trabajo en el análisis filogenético, además de reaprovechar conceptos y métodos consolidados en otras áreas de análisis de sistemas. Para ello proponemos el uso de “model checking”, una técnica de verificación automática madura en el mundo de la verificación. Nuestra aproximación se sustenta sobre tres pilares principales. Primero, el modelado de la dinámica evolutiva es análogamente equivalente al modelado de un sistema de transiciones, donde las características biológicas de las especies (ADN, fenotipo, etc) definen las variables de los estados; y la mutación o salto entre especies se corresponde con la ejecución de una transición. Segundo, el uso de lógicas temporales sistematiza el proceso de formulación y aporta formalismo a la especificación de propiedades filogenéticas. Por último, la verificación de estas fórmulas se realiza de manera automática por cualquiera de las herramientas informáticas existentes, devolviendo un contraejemplo en el caso de resultar falsas. Además de la aportación teórica, hemos evaluado empíricamente las prestaciones del sistema sobre una herramienta software de model checking real: SMV. Esta tecnología ha demostrado ser viable cuando trabaja aisladamente con genes o fragmentos de ADNmt, ya que su tamaño no es excesivamente grande. Sin embargo, su coste temporal escala cuadráticamente con la longitud de las secuencias, mientras que el consumo de memoria crece linealmente hasta alcanzar más de 2,5 GBytes en el caso peor. Por estos motivos, en estudios filogenéticos futuros sobre el ADNmt completo (o el ADN nuclear, que es más grande) será necesario paralelizar y componer la solución a partir de los resultados parciales. También se ha propuesto una estructura de datos basada en los diagramas de decisión para manejar cadenas de ADNmt de forma más eficiente en memoria a cómo se realiza en la actualidad. 000005302 521__ $$aIngeniero en Informática 000005302 540__ $$aDerechos regulados por licencia Creative Commons 000005302 6531_ $$aAnálisis filogenético 000005302 6531_ $$aVerificación formal 000005302 6531_ $$aLógica temporal 000005302 6531_ $$aModel checking 000005302 700__ $$aColom Piazuelo, José Manuel$$edir. 000005302 7102_ $$aUniversidad de Zaragoza$$bInformática e Ingeniería de Sistemas$$cLenguajes y Sistemas Informáticos 000005302 830__ $$aCPS 000005302 8560_ $$fnrequeno@unizar.es 000005302 8564_ $$s1071575$$uhttps://zaguan.unizar.es/record/5302/files/TAZ-TFM-2010-075.pdf$$yMemoria (spa) 000005302 909CO $$ooai:zaguan.unizar.es:5302$$ptrabajos-fin-master$$pdriver 000005302 950__ $$a 000005302 980__ $$aTAZ$$bTFM$$cCPS