Facultad Regional Santa Fe

Permanent URI for this communityhttp://48.217.138.120/handle/20.500.12272/113

Browse

Author: search.filters.author.Roa, JorgeHas files: Yes

Search Results

Now showing 1 - 4 of 4
  • Thumbnail Image
    Item
    Tool for the verification of BPMN models based on anti-patterns
    (2015) Orsi, Maximiliano; Roa, Jorge
    The verification of the behavior of business process models is an important requirement for Business Process Management. In this work, a verification tool based on behavioral anti-patterns for the verification of BPMN business process models is proposed. The purpose is to provide support to business analysts and system designers to perform verification of the control flow of business process models. The tool will be implemented as a plug-in of the Oryx platform and will determine whether process models are free from errors like deadlocks and lacks of synchronizations.
  • Thumbnail Image
    Item
    Detection of anti-patterns in the control flow of collaborative business processes
    (2015) Chiotti, Omar; Roa, Jorge; Villarreal, Pablo
    The verification of the behavior of Collaborative Business Processes is an important aspect to consider when developing inter-organizational systems. In this work, a verification approach for the control flow of collaborative processes based on anti-patterns is proposed to improve the performance of verification. The approach supports the verification of complex constructs for advanced synchronization, multiple instances, and exception management. To this aim, 10 anti-patterns were defined from a repository of process models, and a tool which implements the anti-patterns was developed to evaluate the verification approach. Results indicate that, at worst, the verification time is less than half a millisecond, even for models with complex control flow constructs.
  • Thumbnail Image
    Item
    Verification of structured processes : a method based on unsoundness profile
    (2013) Villarreal, Pablo; Roa, Jorge; Chiotti, Omar
    The verification of business processes has been widely studied in the last two decades achieving significant results. Despite this, existing verification tech-niques based on state space exploration suffer, for large processes, the state space explosion problem. New techniques improved verification performance by structuring processes as trees. However, they do not support complex con-structs for advanced synchronization and exception management. To cope with this issue we propose the definition of an unsoundness profile of a given pro-cess language, which specifies all possible combinations of control flow con-structs that can lead to errors in the behavior of structured processes defined with such a language. In addition, we introduce the sequential and hierarchical soundness properties, which make use of this profile to determine soundness of a structured process with complex constructs in polynomial time. As an exam-ple, we defined an unsoundness profile for a subset of the BPMN language and verified the behavior of a BPMN process model.
  • Thumbnail Image
    Item
    Verificación y alineación de procesos de negocio colaborativos
    (2014-02) Roa, Jorge; Villareal, Pablo; Chiotti, Omar
    Las colaboraciones inter-organizacionales permiten nuevas formas de gestión basadas en la cooperación. Los sistemas de información que brindan soporte a la gestión de estas acciones de colaboración requieren definir modelos y especificaciones de procesos de negocio colaborativos (PNCs) que representan el comportamiento explícito de la colaboración. En base a técnicas formales y a los conceptos del desarrollo dirigido por modelos, en esta tesis se proponen métodos y herramientas que permiten determinar el correcto comportamiento de los modelos de PNCs y, a partir de dichos modelos, generar especificaciones de PNCs cuyo comportamiento está alineado con el de los modelos. Se propone el lenguaje formal Redes de Interacción Global (GI-Nets) y un método de transformación para definir modelos formales de PNCs con GI-Nets a partir de modelos conceptuales de PNCs. Se definen dos métodos de verificación que permiten determinar si un modelo de PNC satisface un conjunto de propiedades que determinan su correcto comportamiento. El primer método, basado en GI-Nets, propone la propiedad de Solidez de Interacción Global de una GI-Net como principal criterio de verificación. Este método permite detectar el lugar específico donde existe un bloqueo en un modelo de PNC. El segundo método, basado en anti-patrones de comportamiento, provee un enfoque para especificar en forma sistemática los anti-patrones de cualquier lenguaje de PNCs. Este método detecta el lugar de un bloqueo y determina el conjunto de elementos que lo produce. Ambos métodos pueden ser utilizados con cualquier lenguaje de PNCs y dan soporte a la verificación de PNCs con constructores complejos. Se define un método formal de transformación de modelos que permite generar en forma automática una especificación de PNC cuyo comportamiento esté alineado con el definido en el modelo conceptual del PNC a partir del cual fue generada. Esto implica que el comportamiento de la especificación será correcto si el comportamiento del modelo del PNC es correcto, y viceversa. El método se utiliza para generar especificaciones de PNCs basadas en tecnologías de servicios Web a partir de modelos conceptuales de PNCs. Finalmente, se presentan las herramientas desarrolladas para la formalización, verificación y transformación de modelos y especificaciones de PNCs, y se utilizan las mismas para evaluar y validar los métodos propuestos en la tesis.