Especificación formal y verificación de propiedades temporales de procesos de negocios

Institución otorgante:

Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales

Fecha:

2014

Tipo de documento: 

info:eu-repo/semantics/doctoralThesis
 

Formato:

application/pdf

Idioma:

spa

Temas:

PROCESOS DE NEGOCIOS - WORKFLOWS - LOGICAS TEMPORALES - FLUENTES - ANALISIS AUTOMATICO - MODEL CHECKING - BUSINESS PROCESS - WORKFLOWS - TEMPORAL LOGICS - FLUENTS - AUTOMATIC ANALYSIS - MODEL CHECKING

Descripción:

El uso de diferentes métodos y herramientas que asistan en la organización y el control de procesos, ha tomado relevancia debido a la necesidadconstante de eficiencia por parte de la industria y a la adecuación de sus prácticasa las emergentes y novedosas técnicas de desarrollo y producción. Como productode estas necesidades, diversos lenguajes para la descripción de procesos de negocioscapturaron el interés tanto del sector productivo, para su aplicación en sus actividades,como así también del sector académico, con el fin de aportar conocimiento ygenerar nuevas herramientas para tal fin. Si bien la mayor parte de los lenguajes para la especificación de procesos denegocios son informales, existen algunos fundados en formalismos matemáticos. Estobrinda a estos lenguajes formales para procesos de negocios la eliminación deambigüedades en la interpretación de especificaciones, y la posibilidad de realizardiferentes análisis formales, como chequeos de sanidad. Sin embargo, las alternativasexistentes poseen en general limitaciones, o bien en poder expresivo, o, para lasalternativas más expresivas, la imposibilidad de realizar algunas tareas de análisisautomáticamente. En este trabajo presentamos un enfoque formal para la especificación y el análisis de procesos de negocios, que permite dar semántica a construccionescomplejas de procesos de negocios, a la vez que admite el análisis de chequeos desanidad usuales de manera automática mediante model checking. Más aún, nuestrapropuesta abarca la posibilidad de que el usuario especifique y analice propiedadesde interés acerca de las especificaciones, mediante lógicas temporales, un mecanismocon frecuencia ausente en los lenguajes existentes. Además del desarrollo de una semántica formal para un lenguaje de proceso denegocios sumamente expresivo, nuestro trabajo toma como base para la especificación de propiedades de procesos de negocios el uso de lógicas temporales. Identificamosalgunos elementos que hacen particularmente complicada la expresión dealgunos tipos de propiedades, en particular cuando las mismas demandan expresarrepeticiones de eventos o tareas, y proponemos una lógica temporal que permitedescribir tales propiedades con mayor facilidad. Con el fin de no perder capacidadde análisis, desarrollamos traducciones que nos permiten capturar los elementosnovedosos de esta lógica en términos de otros elementos, soportados por lógicas temporales tradicionales, con soporte de herramientas. Por otra parte, observamosla tendencia de los lenguajes de descripción de procesos de negocios a no tratar formalmentela descripción de los productos que manipulan. Tomamos un formalismoexcepcional en este sentido, PPML, y definimos a partir del mismo un lenguaje deespecificaciones, una semántica simplificada para el mismo, y una técnica de análisisde especificaciones basada en una caracterización de sus modelos en UPPAAL. Nuestro enfoque está claramente orientado a la producción de herramientas desoporte al proceso de especificación. Para los lenguajes tratados brindamos herramientasde especificación y análisis de procesos de negocios, como así también laposibilidad de construir descripciones de procesos de negocios a partir de las propiedadesque los mismos deben cumplir. Estas tareas son evaluadas en este trabajoa través del desarrollo de casos de estudio tomados de la literatura del área, en loque respecta a descripción de procesos y chequeos de sanidad de los mismos, y enbase a variantes de estos casos en las cuales se enfatiza la necesidad de contar conpropiedades descriptas por el usuario, y de dar más relevancia a la descripción delos productos manipulados por los procesos de negocios.

Identificador:

https://hdl.handle.net/20.500.12110/tesis_n5429_Regis