Universidade Federal de Uberlândia
Programa de Pós-Graduação em Ciência da Computação
Formalização de Workflow baseada na
Lógica Linear: Análise Qualitativa e
Quantitativa
Lígia Maria Soares Passos
Aluna
Stéphane Julia
Orientador
Agenda

Fundamentação teórica

Redes de Petri



Workflow nets








Soundness
Processo
Roteamento
Acionamento
Lógica Linear


Elementos básicos
Redes de Petri T-temporais
Árvores de Prova Canônica
Trabalhos relacionados
Metodologia
Resultados esperados
Estado atual do trabalho
2
Redes de Petri

Redes de Petri – elementos
básicos:
Lugar;
 Transição;
 Ficha;
 Arcos;


Ficha
Lugar
Arcos
Transição
Redes de Petri t-temporais

Associa-se às transições
uma duração de
sensibilização. Um
intervalo [θmin, θmax] é
associado a cada
transição.
[2,5]
3
WorkFlow net
Caso já
tratado
Tarefas
Caso a ser
tratado
c3
c1
Contact_Client
Record
Pay
c5
c6
Collect
c7
Start
Assess
c2
End
c4
Contact_Department
Lugar de
Início
File
Send_Letter
Condições
Lugar de
Término
4
WorkFlow net
Processo, Roteamento, Acionamento
Acionadas por recursos
Condicional
Sequencial
c3
c1
Contact_Client
Record
Pay
c5
c6
Collect
c7
Start
Assess
c2
File
End
c4
Contact_Department
Send_Letter
Paralela
5
WorkFlow net
Soundness
c3
c1
Contact_Client
Record
Pay
c5
c6
Collect
c7
Start
Assess
c2
File
End
c4
Contact_Department
Send_Letter
Esta WorkFlow net é Sound
6
WorkFlow net
Soundness
Esta WorkFlow net não é Sound
7
Lógica Linear
 Proposta
em 1987 por Girard.
 Proposições (átomos) são tratados como recursos.
 Conectivos Multiplicativos
 ⊗, chamado vezes (times), representa a
conjunção multiplicativa e expressa AND
(disponibilidade simultânea) de recursos. Ex.
A⊗B.
 ⊸, chamado implicação linear, expressa
dependência causal entre recursos. Ex. A ⊸B.
8
Tradução de uma RdP em fórmulas da
Lógica Linear
c3
c1
Contact_Client
Record
Pay
c5
c6
Collect
c7
Start
Assess
c2
File
End
c4
Contact_Department
Send_Letter
Cada ficha da marcação inicial é representada por um átomo com o nome do lugar.
Neste caso, Start.
Cada transição é representada por uma fórmula M1 ⊸ M2, onde M1 e M2 são
marcações. Por ex. Record = Start ⊸ c1⊗c2, Collect = c3⊗c4 ⊸ c5
Um sequente M, ti ⊢M’ representa um cenário onde M e M’ são, respectivamente,
a marcação inicial e final e ti é uma lista de transições não ordenadas.
9
Ex.
Start,Record,ContactClient,ContactDepartment,Collect,Assess,Pay,File ⊢ End
Lógica Linear
Construída de forma bottom-up
Árvores de Prova Canônica
10
Podem incluir cálculo de datas simbólicas para produção e
consumo dos átomos
Trabalhos relacionados
“Scenario duration characterization of t-timed
Petri nets using linear logic” [Pradin-Chezalviel
et al. 1999].
 “Temporal inference of workflow systems based
on time petri nets: Quantitative and qualitative
analysis” [Lin and Qu 2004].
 “Reachability and Temporal Conflicts in t-time
Petri Nets” [Riviere et al. 2001].
 “Workflow Management: Models, Methods and
Systems” [van der Aalst and van Hee 2002].

11
Metodologia

Análise qualitativa
Soundness

prova do critério
Será considerada uma WorkFlow net sem extensão de tempo.
Serão construídas árvores de prova canônica da lógica linear
(sem cálculo de datas), considerando cada rota alternativa da
WorkFlow net. A partir da construção destas árvores de prova
será realizada a análise qualitativa para a WorkFlow net,
provando se a mesma é ou não Sound.
Análise quantitativa
determinar datas
simbólicas para realização das tarefas
(planejamento de recursos)

Será realizada através da construção de árvores de prova
canônica da lógica linear com cálculo de datas para a rede de
Petri t-temporal, com conceitos de WorkFlow net embutidos
(t-Time WorkFlow net), que modela um processo de workflow.
A partir das datas obtidas nas árvores de prova, serão
analisadas as datas de execução de cada tarefa do modelo e
será estabelecido um planejamento dos recursos a serem
utilizados na execução de cada atividade.
12
Resultados esperados
Formalizar processos de workflow utilizando
redes de Petri t-temporais e WorkFlow nets.
 Realizar análises formais (qualitativa e
quantitativa) de processos de workflow
utilizando a lógica linear.
 Estabelecer datas simbólicas para a realização
das tarefas presentes no processo de workflow,
possibilitando o planejamento de recursos.
 Realizar um estudo de caso no contexto de
planejamento de recursos em gestão de projeto
de software.

13
Estado atual do trabalho

Elaboração do artigo “Análise qualitativa e
quantitativa de WorkFlow nets utilizando Lógica
Linear”, que será submetido ao V Simpósio
Brasileiro de Sistemas de Informação (SBSI2009).
14