A aplicação do método para detecção de cenários livres de deadlock em um sistema composto considera a deĄnição e análise de todos os cenários dos módulos que compõem
o sistema composto.
Assim, considerando a noção de um cenário deĄnida neste trabalho, tem-se que para o módulo de workĆow C1, apresentado na Figura 21, existem dois cenários distintos: o primeiro cenário 𝑆𝑐1𝐶1, onde a tarefa t2 será executada e o segundo cenário, 𝑆𝑐2𝐶1, onde a execução da tarefa t3 é considerada. Já para o módulo 𝑇 1, há dois cenários distintos: o primeiro cenário, 𝑆𝑐1𝑇1, onde as tarefas 𝑡4 e 𝑡6 serão executadas e o segundo cenário,
𝑆𝑐2𝑇1, onde as tarefas 𝑡5 e 𝑡7 serão realizadas, conforme mostra a subseção 4.2.1.
Nesta abordagem, cada um destes cenários é então representado por um sequente da Lógica Linear que considera as marcações inicial e Ąnal de um módulo, seus lugares de
input e uma lista não ordenada de transições envolvidas no cenário.
Assim, considerando o módulo de workĆow C1 apresentado na Figura 21, dois cenários distintos (e, consequentemente, sequentes da Lógica Linear) são deĄnidos:
𝑆𝑐1𝐶1 = 𝑞0, 𝑡𝑖𝑐𝑘𝑒𝑡, 𝑡1, 𝑡2 ⊢ 𝑞2,
𝑆𝑐2𝐶1 = 𝑞0, 𝑡𝑖𝑐𝑘𝑒𝑡, 𝑡1, 𝑡3 ⊢ 𝑞2.
Já para o módulo de workĆow T1, mostrado na Figura 21, dois cenários são deĄnidos:
𝑆𝑐1𝑇1 = 𝑝0, 𝑒𝐶𝑎𝑠ℎ, 𝑡4, 𝑡6 ⊢ 𝑝3,
𝑆𝑐2𝑇1 = 𝑝0, 𝑉 𝐼𝑆𝐴, 𝑡5, 𝑡7 ⊢ 𝑝3.
Considerando a adaptação proposta na subseção 4.2.1, estes cenários são um subcon- junto dos cenários deĄnidos para a veriĄcação do critério de correção Soundness para o sistema composto 𝐶1 ⊕ 𝑇 1. Consequentemente, as árvores de prova construídas para pro- var tais cenários, apresentadas no Apêndice A.3, podem ser reutilizadas para a detecção dos cenários livres de deadlock no sistema composto 𝐶1 ⊕ 𝑇 1.
É importante notar que, no contexto da detecção de cenários livres de deadlock, cada árvore de prova da Lógica Linear possui dois sequentes mais relevantes: o primeiro se- quente e o último sequente. Como as árvores de prova da Lógica Linear são construídas e lidas de forma bottom up, o primeiro sequente da árvore de prova para o cenário 𝑆𝑐1𝐶1, mostrada no Apêndice A.3, é 𝑞0, 𝑡𝑖𝑐𝑘𝑒𝑡, 𝑡1, 𝑡2 ⊢ 𝑞2 e o último sequente é 𝑉 𝐼𝑆𝐴, 𝑞2 ⊢ 𝑞2. O átomo 𝑡𝑖𝑐𝑘𝑒𝑡 no primeiro sequente representa o lugar de input para o cenário 𝑆𝑐1𝐶1. Isso signiĄca que, para funcionar corretamente, este cenário consome o átomo 𝑡𝑖𝑐𝑘𝑒𝑡. Já o átomo 𝑉 𝐼𝑆𝐴, no último sequente, corresponde a um átomo produzido pelo cenário
𝑆𝑐1𝐶1, que não foi consumido por nenhuma fórmula de transição deste cenário, isto é, o átomo remanescente na árvore de prova, ou seja, o átomo que representa o lugar de
output para o referido cenário.
Assim, considerando o conjunto de árvores de prova para os cenários 𝑆𝑐1𝐶1, 𝑆𝑐2𝐶1,
𝑆𝑐1𝑇1 e 𝑆𝑐2𝑇1, apresentadas no Apêndice A.3, nota-se que o átomo de input do cenário
𝑆𝑐1𝐶1, 𝑡𝑖𝑐𝑘𝑒𝑡, corresponde ao átomo de output do cenário 𝑆𝑐2𝑇1. Além disso, o átomo de
output do cenário 𝑆𝑐1𝐶1, 𝑉 𝐼𝑆𝐴, corresponde ao átomo de lugar de input para o cenário
𝑆𝑐2𝑇1. Ou seja, 𝑃𝐼(𝑆𝑐1𝐶1)∪𝑃𝐼(𝑆𝑐2𝑇1) = ¶𝑡𝑖𝑐𝑘𝑒𝑡, 𝑉 𝐼𝑆𝐴♢ = 𝑃𝑂(𝑆𝑐1𝐶1)∪𝑃𝑂(𝑆𝑐2𝑇1) = ¶𝑉 𝐼𝑆𝐴, 𝑡𝑖𝑐𝑘𝑒𝑡♢. Já para os cenários 𝑆𝑐2𝐶1 e 𝑆𝑐1𝑇1, tem-se que 𝑃𝐼(𝑆𝑐2𝐶1)∪𝑃𝐼(𝑆𝑐1𝑇1) =
¶𝑡𝑖𝑐𝑘𝑒𝑡, 𝑒𝐶𝑎𝑠ℎ♢ = 𝑃𝑂(𝑆𝑐
2𝐶1) ∪ 𝑃𝑂(𝑆𝑐1𝑇1) = ¶𝑒𝐶𝑎𝑠ℎ, 𝑡𝑖𝑐𝑘𝑒𝑡♢. Desta forma, conside- rando o sistema composto da Figura 22, existem dois cenários candidatos a serem anali- sados: 𝑆𝑐1𝐶1 × 𝑆𝑐2𝑇1 e 𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1.
Deve-se observar que, de acordo com a DeĄnição 11, um sistema composto considera exatamente dois módulos de workĆow. Já a DeĄnição 8, mostra que uma IOWF-net possui 𝑛 LWF-nets. Logo, os cenários candidatos a serem livres de deadlock, no caso da composição de serviços Web, considera a composição de exatamente dois cenários. Assim, considerando o método apresentado na seção 3.4 e o fato de que um sistema composto possui exatamente dois módulos de workĆow, para veriĄcar se um cenário candidato
𝑆𝑐𝑖1 × 𝑆𝑐𝑗2 é, de fato, um cenário livre de deadlock, é necessário provar o sequente da
Lógica Linear que considera as listas de transições dos cenários 𝑆𝑐𝑖1 e 𝑆𝑐𝑗2, as transições
𝑡𝑖 e 𝑡𝑜, juntamente com os lugares globais de início e término 𝑖 e 𝑜, respectivamente,
deĄnidos na DeĄnição 11. Assim, o sequente da Lógica Linear a ser provado é dado por:
𝑖, 𝑡𝑖, Ð, Ñ, 𝑡𝑜 ⊢ 𝑜, onde Ð é a lista de transições para o cenário 𝑆𝑐𝑖1 e Ñ é a lista de transições
para o cenário 𝑆𝑐𝑗2. Assim, para o cenário candidato 𝑆𝑐1𝐶1 × 𝑆𝑐2𝑇1, o seguinte sequente da Lógica Linear deve ser provado: 𝑖, 𝑡𝑖, 𝑡1, 𝑡2, 𝑡5, 𝑡7, 𝑡𝑜 ⊢ 𝑜. Para o cenário candidato
𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1, tem-se o seguinte sequente da Lógica Linear: 𝑖, 𝑡𝑖, 𝑡1, 𝑡3, 𝑡4, 𝑡6, 𝑡𝑜 ⊢ 𝑜.
Considerando as árvores de prova apresentadas no Apêndice A.3, o cenário candidato
𝑆𝑐1𝐶1 × 𝑆𝑐2𝑇1, cujo sequente a ser provado é 𝑖, 𝑡𝑖, 𝑡1, 𝑡2, 𝑡5, 𝑡7, 𝑡𝑜 ⊢ 𝑜, corresponde ao
cenário 𝑆𝑐2𝐶1 ⊕ 𝑇 1. Ou seja, os sequentes da Lógica Linear a serem provados são iguais. Semelhante situação ocorre para o cenário candidato 𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1. O sequente a ser provado para este cenário é 𝑖, 𝑡𝑖, 𝑡1, 𝑡3, 𝑡4, 𝑡6, 𝑡𝑜 ⊢ 𝑜, que é o sequente provado no cenário
𝑆𝑐1𝐶1 ⊕ 𝑇 1, apresentado no Apêndice A.3. Logo, as árvores de prova para os cenários
𝑆𝑐2𝐶1 ⊕ 𝑇 1 e 𝑆𝑐1𝐶1 ⊕ 𝑇 1 apresentadas no Apêndice A.3 podem ser reutilizadas.
Assim, considerando as árvores de prova para os cenários candidatos, deve-se veriĄcar se as condições a) e b), apresentadas na seção 3.4 são satisfeitas para cada um dos cenários candidatos. Caso positivo, o cenário candidato analisado é um cenário livre de deadlock. Considerando as árvores de prova apresentadas para os cenários candidatos, no Apên- dice A.3, nota-se que apenas um átomo o foi produzido em cada árvore de prova. Nota-se também que não há nenhum átomo disponível para consumo no último sequente destas árvores de prova. Logo, prova-se que os dois cenários analisados Ąnalizam corretamente e, quando a execução de qualquer um destes cenários Ąnaliza, não há tarefas remanescentes a serem tratadas. Assim, os cenários 𝑆𝑐1𝐶1 × 𝑆𝑐2𝑇1 e 𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1 são cenários livres de deadlock.
Finalmente, deve-se observar que, considerando o sistema composto da Figura 22, os cenários livres de deadlock detectados podem prover todas as necessidades de negócio entre o cliente (customer) e um serviço de bilheteria (ticket service), isto é, o cenário 𝑆𝑐1𝐶1 ×
𝑆𝑐2𝑇1 é aquele no qual o cliente efetua o pagamento utilizando um cartão de crédito VISA e o cenário 𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1 é aquele no qual dinheiro eletrônico (eCash) é utilizado
como forma de pagamento. Assim, os cenários livres de deadlock formalizam os serviços oferecidos pelo sistema composto. Para uma melhor visualização destes serviços, deve-se considerar o grafo de precedência associado a cada um deles. Para a construção de tais grafos, deve-se considerar as árvores de prova da Lógica Linear rotuladas, apresentadas no Apêndice A.3.1. O primeiro serviço, 𝑆𝑐1𝐶1 × 𝑆𝑐2𝑇1, é formalizado pelo grafo de precedência apresentado na Figura 23. Já o grafo de precedência da Figura 24 formaliza o segundo serviço, 𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1. ii i ti q0 wait for ticket q1 pay by VISA p0 delivery ticket Paid by VISA p2 p3 q2 t o o fi ticket VISA
Figura 23 Ű Grafo de precedência para o serviço 𝑆𝑐1𝐶1 × 𝑆𝑐2𝑇1.
ii i ti q0 wait for ticket q1 pay by eCash p0 delivery ticket Paid by eCash p1 p3 q2 t o o fi ticket eCash
Figura 24 Ű Grafo de precedência para o serviço 𝑆𝑐2𝐶1 × 𝑆𝑐1𝑇1.