Formal specification and temporal properties verification of business processes

Autor: Regis, Germán Enrique
Přispěvatelé: Aguirre, Nazareno Matías, López Pombo, Carlos Gustavo
Jazyk: Spanish; Castilian
Rok vydání: 2014
Předmět:
Zdroj: Biblioteca Digital (UBA-FCEN)
Universidad Nacional de Buenos Aires. Facultad de Ciencias Exactas y Naturales
instacron:UBA-FCEN
Popis: 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.
Databáze: OpenAIRE
Externí odkaz: