000007869 001__ 7869 000007869 005__ 20170831220356.0 000007869 037__ $$aTAZ-TFM-2012-094 000007869 041__ $$aspa 000007869 1001_ $$aGonzález López de Murillas, Eduardo 000007869 24500 $$a"Model checking" paramétrico de "workflows" científicos 000007869 260__ $$aZaragoza$$bUniversidad de Zaragoza$$c2012 000007869 506__ $$aby-nc-sa$$bCreative Commons$$c3.0$$uhttp://creativecommons.org/licenses/by-nc-sa/3.0/ 000007869 520__ $$aLa computación científica ha ganado un creciente interés en los últimos años en áreas afines a las ciencias de la vida. Los workflows científicos son un tipo especial de workflow que se utilizan en escenarios de grandes dimensiones y gran complejidad computacional como modelos climáticos, estructuras biológicas, química, cirugía o simulación de desastres, por ejemplo, y cuya ejecución es un proceso que consume una gran cantidad de tiempo y recursos. Uno de los objetivos principales de la computación científica ha sido la mejora progresiva a través de la introducción de nuevos paradigmas y tecnologías para poder abordar desafíos cada vez más complejos, siendo uno de estos paradigmas la adición de aspectos semánticos a los workflows. Disponer de una serie de herramientas y técnicas que posibiliten el análisis del comportamiento del workflow antes de su ejecución resulta de gran interés. El objetivo de ese análisis es poder garantizar un comportamiento adecuado y correcto, así como verificar la correcta gestión y utilización de los recursos involucrados. El análisis debería permitir la predicción de la calidad de los resultados, así como identificar aquellos parámetros que son necesarios para obtener los resultados esperados. Desde el punto de vista del usuario, la incorporación de aspectos semánticos permite a los científicos realizar una navegación, interrogación, integración y composición de conjuntos de datos y servicios mucho más eficiente. Sin embargo, el análisis del estado del arte en el área de la semántica aplicada a los modelos en la computación científica muestra carencias significativas en el grado de madurez y aplicación de este enfoque, así como la carencia de técnicas y herramientas para su aplicación. Es necesario, por tanto, proponer y desarrollar nuevas técnicas de modelado y análisis que puedan manejar dichos aspectos semánticos. En este Trabajo Fin de Máster se aborda el análisis, diseño y desarrollo de un método y una herramienta de model checking basados en la introducción de aspectos y anotaciones semánticas tanto en los modelos como en las propiedades que deben verificarse. Como resultado, la herramienta COMBAS (COmprobador de Modelos BAsado en Semántica) proporciona un entorno de integración para la verificación de este tipo de modelos y la navegación por las estructuras resultantes del proceso. Para la descripción de los modelos de workflows científicos se ha utilizado una clase de Redes de Petri de alto nivel anotadas con información semántica en RDF, las U-RDF-PN. A lo largo de este trabajo se ha abordado la adición de las técnicas, metodologías y modelos necesarios para extender el framework con análisis paramétrico, que consiste en un análisis mucho más potente y expresivo mediante la utilización de parámetros cuyo valor es indeterminado al inicio del proceso, de forma que es posible estudiar el comportamiento del workflow respecto a los posibles valores de dichos parámetros. Para restringir los valores de los parámetros en cada uno de los caminos de ejecución del workflow se utiliza el concepto de guardas, expresadas en lógica proposicional, en el modelo del workflow. Para ello, es necesario estudiar primero qué herramientas permiten tratar dichas proposiciones, por lo que se analizan los Satisfiability Modulo Theories (SMTs), el estado actual de los estándares relacionados, la flexibilidad de los solvers disponibles y las herramientas que soporten la semántica que se va a aplicar. Finalmente, la viabilidad y usabilidad del enfoque propuesto se ha demostrado mediante su aplicación al análisis del workflow EBI InterProScan, verificando propiedades de interés para el científico sin necesidad de implementar, desplegar ni ejecutar el workflow. 000007869 521__ $$aMáster Universitario en Ingeniería de Sistemas e Informática 000007869 540__ $$aDerechos regulados por licencia Creative Commons 000007869 6531_ $$amodel checking 000007869 6531_ $$ardf 000007869 6531_ $$actl 000007869 6531_ $$ahigh-level petri nets 000007869 6531_ $$alógica proposicional 000007869 700__ $$aFabra Caro, Francisco Javier$$edir. 000007869 7102_ $$aUniversidad de Zaragoza$$bInformática e Ingeniería de Sistemas$$cLenguajes y Sistemas Informáticos 000007869 8560_ $$f543535@celes.unizar.es 000007869 8564_ $$s132256$$uhttps://zaguan.unizar.es/record/7869/files/TAZ-TFM-2012-094_ANE.pdf$$yAnexos (spa) 000007869 8564_ $$s1446731$$uhttps://zaguan.unizar.es/record/7869/files/TAZ-TFM-2012-094.pdf$$yMemoria (spa) 000007869 909CO $$ooai:zaguan.unizar.es:7869$$ptrabajos-fin-master$$pdriver 000007869 950__ $$a 000007869 980__ $$aTAZ$$bTFM$$cEINA