Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work formalizes four methods based on Linear Logic for the verification of interorganizational
workflow processes modelled by Interorganizational Workflow nets, which
are Petri nets that model such processes. The first method is related to the verification of
the Soundness criteria for interorganizational workflow processes. The method is based on
the construction and analysis of Linear Logic proof trees, which represent the local processes
as much as they do the global processes. The second and third methods are related,
respectively to Soundness criteria verification, Relaxed Soundness and Weak Soundness
for the interorganizational workflow processes. These are obtained through the analysis
of reutilized Linear Logic proof trees that have been constructed for the verification of
the Soundness criteria. However, the fourth method has the objective of detecting the
deadlock free scenarios in interorganizational workflow and is based on the construction
and analysis of Linear Logic proof trees, which initially takes into consideration the local
processes and communication between such, and thereafter the candidate scenarios. A
case study is carried out in the context of a Web services composition check, since there
is a close correlation between the modelling of the interorganizational workflow process
and a Web services composition. Therefore, the four methods proposed in the interorganizational
workflow process context, are applied to a Web services composition. The
evaluation of the obtained results shows that the reutilization of Linear Logic proof trees
initially constructed for verifying the Soundness criteria, in fact occurs in the context of
verifying the Relaxed Soundness andWeak Soundness criteria. In addition, the evaluation
shows how the Linear Logic sequents and their proof trees explicitly show the possibilities
for existing collaborations in a Web service composition. An evaluation that takes into
account the number of constructed linear logic proof trees shows that this number can
be significantly reduced in the deadlock-freeness scenarios detection method. An approach
for resource planning based on the symbolic date calculation, which considers data
extracted from Linear Logic proof trees is presented and validated through simulations performed on the CPN tools simulator. Two approaches for the monitoring of deadlockfreeness
scenarios are introduced and show how data obtained from the Linear Logic proof trees can be used to guide the execution of such scenarios. / Este trabalho formaliza quatro métodos baseados na Lógica Linear para verificação
de processos de workflow interorganizacionais modelados por WorkFlow nets interorganizacionais,
que são redes de Petri que modelam tais processos. O primeiro método está
relacionado com a verificação do critério de correção Soundness para processos de workflow
interorganizacionais. O método é baseado na construção e análise de árvores de prova
da Lógica Linear que representam tanto os processos locais quanto o processo global. O
segundo e terceiro métodos estão relacionados, respectivamente, com a verificação dos
critérios de correção Relaxed Soundness e Weak Soundness para processos de workflow interorganizacionais,
e são obtidos através da análise de árvores de prova da Lógica Linear
reutilizadas, construídas para a prova do critério de correção Soundness. Já o quarto método
tem por objetivo a detecção dos cenários livres de deadlock em processos de workflow
interorganizacionais e é baseado na construção e análise de árvores de prova da Lógica
Linear que consideram, inicialmente, os processos locais e as comunicações entre estes e,
posteriormente, os cenários candidatos.
Um estudo de caso é realizado no contexto da verificação de composições de serviços
Web, uma vez que há uma relação estreita entre a modelagem de um processo de
workflow interorganizacional e uma composição de serviços Web. Assim, os quatro métodos
propostos no contexto dos processos de workflow interorganizacionais são aplicados
a uma composição de serviços Web. A avaliação dos resultados mostra que o reuso de
árvores de prova da Lógica Linear construídas inicialmente para a prova do critério de
correção Soundness de fato ocorre no contexto da verificação dos critérios de correção
Relaxed Soundness e Weak Soundness. Além disso, a avaliação mostra como os sequentes
da Lógica Linear e suas árvores de prova explicitam as possibilidades de colaboração
existentes em uma composição de serviços Web. Uma avaliação que leva em conta o número
de árvores de prova da Lógica Linear construídas mostra que este número pode ser
significativamente reduzido no método para detecção de cenários livres de deadlock. Uma abordagem para planejamento de recursos, baseada no cálculo de datas simbólicas,
que considera dados extraídos de árvores de prova da Lógica Linear, é apresentada e validada através de simulações realizadas no simulador CPN Tools. Duas abordagens
para a monitoração dos cenários livres de deadlock são introduzidas e mostram como
dados obtidos nas árvores de prova da Lógica Linear podem ser utilizados para guiar a
execução de tais cenários. / Doutor em Ciência da Computação
| Identifer | oai:union.ndltd.org:IBICT/urn:repox.ist.utl.pt:RI_UFU:oai:repositorio.ufu.br:123456789/12458 |
| Date | 22 February 2016 |
| Creators | Passos, Lígia Maria Soares |
| Contributors | Julia, Stéphane, Rosa, Pedro Frosi, Lopes, Carlos Roberto, Miyagi, Paulo Eigi, Villani, Emilia |
| Publisher | Universidade Federal de Uberlândia, Programa de Pós-graduação em Ciência da Computação, UFU, BR, Ciências Exatas e da Terra |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFU, instname:Universidade Federal de Uberlândia, instacron:UFU |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0026 seconds