TAZ-TFM-2012-094


"Model checking" paramétrico de "workflows" científicos

González López de Murillas, Eduardo
Fabra Caro, Francisco Javier (dir.)

Universidad de Zaragoza, EINA, 2012
Informática e Ingeniería de Sistemas department, Lenguajes y Sistemas Informáticos area

Máster Universitario en Ingeniería de Sistemas e Informática

Abstract: La 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.


Free keyword(s): model checking ; rdf ; ctl ; high-level petri nets ; lógica proposicional
Tipo de Trabajo Académico: Trabajo Fin de Master

Creative Commons License

El registro pertenece a las siguientes colecciones:
Academic Works > Trabajos Académicos por Centro > escuela-de-ingeniería-y-arquitectura
Academic Works > End-of-master works



Back to search

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)