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

Mostrar todas las versiones(3)

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 pr...

Descripción completa

Guardado en:
Detalles Bibliográficos
Autor principal: Regis, Germán Enrique
Formato: Tesis Doctoral
Lenguaje:Español
Publicado: 2014
Materias:
PROCESOS DE NEGOCIOS
WORKFLOWS
LOGICAS TEMPORALES
FLUENTES
ANALISIS AUTOMATICO
MODEL CHECKING
BUSINESS PROCESS
TEMPORAL LOGICS
FLUENTS
AUTOMATIC ANALYSIS
Acceso en línea:https://hdl.handle.net/20.500.12110/tesis_n5429_Regis
Aporte de:
Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA) de Universidad de Buenos Aires
id todo:tesis_n5429_Regis
record_format dspace
institution Universidad de Buenos Aires
institution_str I-28
repository_str R-134
collection Biblioteca Digital - Facultad de Ciencias Exactas y Naturales (UBA)
language Español
orig_language_str_mv Español
topic PROCESOS DE NEGOCIOS
WORKFLOWS
LOGICAS TEMPORALES
FLUENTES
ANALISIS AUTOMATICO
MODEL CHECKING
BUSINESS PROCESS
WORKFLOWS
TEMPORAL LOGICS
FLUENTS
AUTOMATIC ANALYSIS
MODEL CHECKING
spellingShingle PROCESOS DE NEGOCIOS
WORKFLOWS
LOGICAS TEMPORALES
FLUENTES
ANALISIS AUTOMATICO
MODEL CHECKING
BUSINESS PROCESS
WORKFLOWS
TEMPORAL LOGICS
FLUENTS
AUTOMATIC ANALYSIS
MODEL CHECKING
Regis, Germán Enrique
Especificación formal y verificación de propiedades temporales de procesos de negocios
topic_facet PROCESOS DE NEGOCIOS
WORKFLOWS
LOGICAS TEMPORALES
FLUENTES
ANALISIS AUTOMATICO
MODEL CHECKING
BUSINESS PROCESS
WORKFLOWS
TEMPORAL LOGICS
FLUENTS
AUTOMATIC ANALYSIS
MODEL CHECKING
description 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.
format Tesis Doctoral
author Regis, Germán Enrique
author_facet Regis, Germán Enrique
author_sort Regis, Germán Enrique
title Especificación formal y verificación de propiedades temporales de procesos de negocios
title_short Especificación formal y verificación de propiedades temporales de procesos de negocios
title_full Especificación formal y verificación de propiedades temporales de procesos de negocios
title_fullStr Especificación formal y verificación de propiedades temporales de procesos de negocios
title_full_unstemmed Especificación formal y verificación de propiedades temporales de procesos de negocios
title_sort especificación formal y verificación de propiedades temporales de procesos de negocios
publishDate 2014
url https://hdl.handle.net/20.500.12110/tesis_n5429_Regis
work_keys_str_mv AT regisgermanenrique especificacionformalyverificaciondepropiedadestemporalesdeprocesosdenegocios
AT regisgermanenrique formalspecificationandtemporalpropertiesverificationofbusinessprocesses
_version_ 1782027310395817984
spelling todo:tesis_n5429_Regis2023-10-03T12:57:08Z Especificación formal y verificación de propiedades temporales de procesos de negocios Formal specification and temporal properties verification of business processes Regis, Germán Enrique PROCESOS DE NEGOCIOS WORKFLOWS LOGICAS TEMPORALES FLUENTES ANALISIS AUTOMATICO MODEL CHECKING BUSINESS PROCESS WORKFLOWS TEMPORAL LOGICS FLUENTS AUTOMATIC ANALYSIS MODEL CHECKING 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. The use of methods and tools to assist in process organization andcontrol is receiving increasing attention. This is due to the constant need for efficiencyin industry, and the pressure on industry to adopt emergent developmentand production techniques, and adapt current practices to these emergent technologies. As a consequence, various languages for describing business processes haveattracted both industry, which applies them in its activities, and academia, whichcan contribute knowledge and help provide novel tools for these languages. Even though most languages for business process specification are informal, someof these languages are founded on mathematical formalisms. Formal business processspecification languages profit from the elimination of ambiguities in the interpretationof their specifications, and the possibility of performing different kinds of formalanalyses, such as soundess checks. However, the available formal alternatives havelimitations, either in expressive power, or, in the case of the more expressive formalisms,the impossibility of performing some analysis tasks fully automatically. Inthis work we present a formal approach for the specification and analysis of businessprocesses, that allows us to provide suitable semantics to complex constructions inbusiness process specifications, while at the same time allowing us to perform typicalsoundness checks fully automatically via model checking. Moreover, our approachincludes the possibility of enabling users to specify and analyze properties of theirinterest about specifications, using temporal logics, a mechanism often missing fromexisting languages. Besides the development of a formal semantics for a very expressive businessprocess language, our work is based on the use of temporal logics for specifyingproperties of business processes. We identify some elements that make it difficult toexpress some kinds of properties, in particular those demanding referring to repetitionsof events or tasks, and propose a temporal logic that allows us to specify theseproperties more conveniently. In order to maintain the possibility of automaticallyanalyzing specifications, we develop translations that enable us to capture the novelelements in our logic in terms of other elements, supported by traditional temporallogics with tool support. Also, we observe a tendency in business process languagesto disregard, in their formalizations, the description of the products that processes manipulate. We take a formalism that is exceptional in this respect, PPML, anddefine a formal specification language in terms of it, a simplified semantics for it,and an analysis technique for its specifications, based on a characterization of itsmodels in UPPAAL. Our approach is clearly oriented towards producing tool support for businessprocess specification. For the languages that we deal with in this work, we providetools for business process specification, property specification, and automatedanalysis. We also enable the user to build business process descriptions from theproperties these processes are required to fullfil. These tasks are assessed in ourwork via case studies taken from the literature, for the case of business process descriptionand soundness checks, and variants of these case studies in which the needof referring to event repetitions, and the role of products in process descriptions, areemphasized. Fil: Regis, Germán Enrique. Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales; Argentina. 2014 Tesis Doctoral PDF Español info:eu-repo/semantics/openAccess https://creativecommons.org/licenses/by-nc-sa/2.5/ar https://hdl.handle.net/20.500.12110/tesis_n5429_Regis

Ejemplares similares