Tesis > Documento


Ver el documento (formato PDF)   Regis, Germán Enrique.  "Especificación formal y verificación de propiedades temporales de procesos de negocios"  (2014)
Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
URL:
     
Resumen:
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 necesidad constante de eficiencia por parte de la industria y a la adecuación de sus prácticas a las emergentes y novedosas técnicas de desarrollo y producción. Como producto de estas necesidades, diversos lenguajes para la descripción de procesos de negocios capturaron 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 y generar nuevas herramientas para tal fin. Si bien la mayor parte de los lenguajes para la especificación de procesos de negocios son informales, existen algunos fundados en formalismos matemáticos. Esto brinda a estos lenguajes formales para procesos de negocios la eliminación de ambigüedades en la interpretación de especificaciones, y la posibilidad de realizar diferentes análisis formales, como chequeos de sanidad. Sin embargo, las alternativas existentes poseen en general limitaciones, o bien en poder expresivo, o, para las alternativas más expresivas, la imposibilidad de realizar algunas tareas de análisis automá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 construcciones complejas de procesos de negocios, a la vez que admite el análisis de chequeos de sanidad usuales de manera automática mediante model checking. Más aún, nuestra propuesta abarca la posibilidad de que el usuario especifique y analice propiedades de interés acerca de las especificaciones, mediante lógicas temporales, un mecanismo con frecuencia ausente en los lenguajes existentes. Además del desarrollo de una semántica formal para un lenguaje de proceso de negocios sumamente expresivo, nuestro trabajo toma como base para la especificación de propiedades de procesos de negocios el uso de lógicas temporales. Identificamos algunos elementos que hacen particularmente complicada la expresión de algunos tipos de propiedades, en particular cuando las mismas demandan expresar repeticiones de eventos o tareas, y proponemos una lógica temporal que permite describir tales propiedades con mayor facilidad. Con el fin de no perder capacidad de análisis, desarrollamos traducciones que nos permiten capturar los elementos novedosos de esta lógica en términos de otros elementos, soportados por lógicas temporales tradicionales, con soporte de herramientas. Por otra parte, observamos la tendencia de los lenguajes de descripción de procesos de negocios a no tratar formalmente la descripción de los productos que manipulan. Tomamos un formalismo excepcional en este sentido, PPML, y definimos a partir del mismo un lenguaje de especificaciones, una semántica simplificada para el mismo, y una técnica de análisis de especificaciones basada en una caracterización de sus modelos en UPPAAL. Nuestro enfoque está claramente orientado a la producción de herramientas de soporte al proceso de especificación. Para los lenguajes tratados brindamos herramientas de especificación y análisis de procesos de negocios, como así también la posibilidad de construir descripciones de procesos de negocios a partir de las propiedades que los mismos deben cumplir. Estas tareas son evaluadas en este trabajo a través del desarrollo de casos de estudio tomados de la literatura del área, en lo que respecta a descripción de procesos y chequeos de sanidad de los mismos, y en base a variantes de estos casos en las cuales se enfatiza la necesidad de contar con propiedades descriptas por el usuario, y de dar más relevancia a la descripción de los productos manipulados por los procesos de negocios.

Abstract:
The use of methods and tools to assist in process organization and control is receiving increasing attention. This is due to the constant need for efficiency in industry, and the pressure on industry to adopt emergent development and production techniques, and adapt current practices to these emergent technologies. As a consequence, various languages for describing business processes have attracted both industry, which applies them in its activities, and academia, which can contribute knowledge and help provide novel tools for these languages. Even though most languages for business process specification are informal, some of these languages are founded on mathematical formalisms. Formal business process specification languages profit from the elimination of ambiguities in the interpretation of their specifications, and the possibility of performing different kinds of formal analyses, such as soundess checks. However, the available formal alternatives have limitations, either in expressive power, or, in the case of the more expressive formalisms, the impossibility of performing some analysis tasks fully automatically. In this work we present a formal approach for the specification and analysis of business processes, that allows us to provide suitable semantics to complex constructions in business process specifications, while at the same time allowing us to perform typical soundness checks fully automatically via model checking. Moreover, our approach includes the possibility of enabling users to specify and analyze properties of their interest about specifications, using temporal logics, a mechanism often missing from existing languages. Besides the development of a formal semantics for a very expressive business process language, our work is based on the use of temporal logics for specifying properties of business processes. We identify some elements that make it difficult to express some kinds of properties, in particular those demanding referring to repetitions of events or tasks, and propose a temporal logic that allows us to specify these properties more conveniently. In order to maintain the possibility of automatically analyzing specifications, we develop translations that enable us to capture the novel elements in our logic in terms of other elements, supported by traditional temporal logics with tool support. Also, we observe a tendency in business process languages to disregard, in their formalizations, the description of the products that processes manipulate. We take a formalism that is exceptional in this respect, PPML, and define 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 its models in UPPAAL. Our approach is clearly oriented towards producing tool support for business process specification. For the languages that we deal with in this work, we provide tools for business process specification, property specification, and automated analysis. We also enable the user to build business process descriptions from the properties these processes are required to fullfil. These tasks are assessed in our work via case studies taken from the literature, for the case of business process description and soundness checks, and variants of these case studies in which the need of referring to event repetitions, and the role of products in process descriptions, are emphasized.

* A este resumen le pueden faltar caracteres especiales. Consulte la versión completa en el documento en formato PDF

Registro:
Título : Especificación formal y verificación de propiedades temporales de procesos de negocios     =    Formal specification and temporal properties verification of business processes
Autor : Regis, Germán Enrique
Director : Aguirre, Nazareno Matías
López Pombo, Carlos Gustavo
Jurados : Braberman, Víctor  ; D’Argenio, Pedro  ; Rossi, Gustavo
Año : 2014
Editor : Facultad de Ciencias Exactas y Naturales. Universidad de Buenos Aires
Filiación : Universidad de Buenos Aires. Facultad de Ciencias Exactas y Naturales
Universidad Nacional de Río Cuarto. Facultad de Ciencias Exactas Físico-Químicas y Naturales. Departamento de Computación
Grado obtenido : Doctor de la Universidad de Buenos Aires en el área de Ciencias de la Computación
Ubicación : Preservación - http://digital.bl.fcen.uba.ar/gsdl-282/cgi-bin/library.cgi?a=d&c=tesis&d=Tesis_5429_Regis
Idioma : Español
Area Temática : Computación / Modelos Computacionales
Palabras claves : PROCESOS DE NEGOCIOS; WORKFLOWS; LOGICAS TEMPORALES; FLUENTES; ANALISIS AUTOMATICO; MODEL CHECKING; BUSINESS PROCESS; WORKFLOWS; TEMPORAL LOGICS; FLUENTS; AUTOMATIC ANALYSIS; MODEL CHECKING
URL al Documento : 
URL al Registro : 
hola chau _gs.DocumentHeader_ chau2 _documentheader_ chau3
Estadísticas:
     http://digital.bl.fcen.uba.ar
Biblioteca Central Dr. Luis Federico Leloir - Facultad de Ciencias Exactas y Naturales - Universidad de Buenos Aires
Intendente Güiraldes 2160 - Ciudad Universitaria - Pabellón II - C1428EGA - Tel. (54 11) 4789-9293 int 34