Submitted by Isaac Francisco de Souza Dias (isaac.souzadias@ufpe.br) on 2016-01-19T16:53:05Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese Renata medeiros.pdf: 1872679 bytes, checksum: 3fce0bb9b510de65d967fa12ff61f596 (MD5) / Made available in DSpace on 2016-01-19T16:53:05Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) tese Renata medeiros.pdf: 1872679 bytes, checksum: 3fce0bb9b510de65d967fa12ff61f596 (MD5) Previous issue date: 2015-03-13 / CNPq / Processos de Negócio Declarativos oferecem mais flexibilidade a processos de negócios pelo uso de regras. Tais regras de negócio descrevem o que deve ou não ser feito durante a execução do processo, mas não especifica como. Para experimentar os benefícios desta abordagem de modelagem, as empresas precisam utilizar uma engine de regras capaz de checar as regras e guiar o usuário durante a execução do processo. As engines de regras disponíveis apresentam várias limitações que impedem seu uso para esta aplicação. Em especial, a conhecida abordagem que emprega Lógica Temporal (Linear Temporal Logic - LTL) tem a desvantagem do problema de explosão do espaço de estados à medida que o modelo do processo cresce. Este trabalho propõe uma nova modelagem de regras baseada em grafos, chamada REFlex, que não compartilha os problemas apresentados pelos outros trabalhos, sendo mais adequada para modelar processos de negócios declarativos do que as técnicas atualmente utilizadas. Para complementar a notação existente que representa atividades e regras no REFlex, foi introduzida a ideia de condições de existência, que permite a definição de regras dependente de dados. Isso não altera o fluxo semântico ou a abordagem sintática da modelagem. Tais condições de existência provêm poder expressivo para processos de negócio declarativos. Neste trabalho, é apresentado o modelo de especificação formal do REFlex utilizando a linguagem Alloy, descrevendo como ela representa o processo de negócio como um grafo e como esse grafo é modelado e atualizado. É introduzido um mecanisno de vivacidade do processo. A conceitualização desse mecanismo foi possível devido à habilidade do Alloy de prover não apenas as situações de impasse mas também o caminho descrevendo como essas situações foram atingidas. Então, esse mecanismo de vivacidade cria as condições necessárias para guiar/controlar as escolhas do usuário, previnindo-o de guiar o processo erroneamente para tais situações de impasse. / Declarative Business Processes offer more flexibility to business processes by the use of business rules. Such business rules describe what must or must not be done during the process execution, but do not prescribe how. To fully experience the benefits of this modeling approach, companies need a rule engine capable of checking the rules and guiding the user through the execution of the process. The rule engines available today present several limitations that impair their use to this application. In particular, the well-known approach that employs Linear Temporal Logic (LTL) has the drawback of the state space explosion as the process model grows. This work proposes a novel graph-based modeling, called REFlex, that does not share the problems presented by other works, being better suited to model declarative business processes than the techniques currently in use. To complement the existing notation that represents activities and rules in REFlex we introduce the idea of existence conditions, which allows the definition of data-aware rules. This does not alter the semantic flow or syntactic approach to the precedent modeling. Such existence conditions provide expressive power to declarative business processes. Herein, we present the formal specification model of the REFlex using the Alloy language, describing how it represents the business process as a graph and how this graph is modeled and updated. We introduce a liveness-enforcing mechanism. The conceptualization of this mechanism was possible due to the ability of Alloy to provide not only the activities in deadlock but also the trace describing how these situations were achieved. Hence, the liveness-enforcing mechanism creates the necessary conditions to guide/control the choices taken by the user preventing him from mistakenly driving the process into such deadlock situations.