Facultad Regional Santa Fe

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

Browse

Filters

2013 - 20152

Settings

Author: search.filters.author.Villarreal, PabloSubject: search.filters.subject.Correctness properties

Search Results

Now showing 1 - 2 of 2
  • 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.