Especificación y verificación de propiedades sobre workflows con lógica de fluentes

Abstract

En el presente trabajo proponemos el uso de una l ógica temporal conocida, fluent linear temporal logic (FLTL), para expresar formalmente propiedades sobre flujos de trabajo (work ows). Creemos que esta l ógica es adecuada para dicha tarea, ya que el uso de fluentes nos permite caracterizar de manera flexible estados abtractos para represetación de actividades y restricciones sobre work ows. Con el n de utilizar herramientas autom áticas para el an álisis de estas propiedades, nos focalizamos en una caracterizacióon de workflows como sistemas de transici ón de estados etiquetados, que modela las tareas de un modo conveniente y aprovecha las f órmulas de FLTL. M as a un, auto- matizamos la codi ficaci ón y empleamos model checking, utilizando LTSA (Labeled Transition System Analyzer), para garantizar que un work ow satisface una propiedad dada, o en caso contrario, generar una ejecuci ón que exhiba la violaci ón de la misma.