Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / This work presents a method for qualitative and quantitative analysis of WorkFlow
nets based on the proof trees of linear logic, and an approach for the verification of
workflow specifications in UML through the transformation of UML Activity Diagrams
into WorkFlow nets.
The qualitative analysis is concerned with the proof of soundness correctness criterion
defined for WorkFlow nets.
The quantitative analysis is based on the computation of symbolic dates for the planning
of resources used to handle each task of the workflow process modeled by a t-Time
WorkFlow net.
For the verification of the specifications of workflow processes mapped into UML
Activity Diagrams are presented formal rules to transform this ones into WorkFlow nets.
In this context is proposed the analysis and correction of critical points in UML Activity
Diagrams through the analysis of proof trees of linear logic.
The advantages of such an approach are diverse. The fact of working with linear
logic permits one to prove the correctness criterion soundness in a linear time without
considering the construction of the reachability graph, considering the proper structure
of the WorkFlow net instead of considering the corresponding automata.
Moreover, the computation of symbolic dates for the execution of each task mapped
into the t-Time WorkFlow net permits to plan the utilization of the resources involved
in the activities of the workflow process, through formulas that can be used for any case
handled by the correspondent workflow process, without to examine again the process to
recalculate, for each new case, the dates of start and conclusion for the activities involved
in the process.
Regarding the verification of workflow processes mapped into UML Activity Diagrams,
the major advantage of this approach is the transformation of a semi-formal model into
a formal model, such that some properties, like soundness, can be formally verified. / Este trabalho apresenta um método para a análise qualitativa e quantitativa de Work-
Flow nets baseado nas árvores de prova canônica da lógica linear e uma abordagem para a
verificação de especificações de processos de workflow em UML através da transformação
de Diagramas de Atividades da UML em WorkFlow nets.
A análise qualitativa refere-se à prova do critério de corretude soundness definido para
WorkFlow nets.
Já a análise quantitativa preocupa-se com o planejamento de recursos para cada atividade
de um processo de workflow mapeado em uma t-Time WorkFlow net e baseia-se no
cálculo de datas simbólicas para o planejamento de recursos utilizados na realização de
cada tarefa do processo de workflow.
Para a verificação das especificações de processos de workflow mapeados em Diagramas
de Atividades da UML são apresentadas regras formais para transformar estes diagramas
em WorkFlow nets. Neste contexto também é proposta a análise e correção de pontos
críticos em Diagramas de Atividades da UML através da análise de árvores de prova
canônica da lógica linear.
As vantagens das abordagens apresentadas neste trabalho são diversas. O fato de trabalhar
com lógica linear permite provar o critério de corretude soundness em tempo linear
e sem que seja necessária a construção de um grafo das marcações acessíveis, considerando
diretamente a própria estrutura da WorkFlow net, ao invés de considerar o seu autômato
correspondente.
Além disso, o cálculo de datas simbólicas correspondentes à execução de cada tarefa
mapeada em uma t-Time WorkFlow net permite planejar a utilização dos recursos envolvidos
nas atividades do processo de workflow, através de fórmulas que podem ser
utilizadas por qualquer caso tratado pelo processo de workflow correspondente, sem que
seja necessário percorrer novamente o processo de workflow inteiro para recalcular, para
cada novo caso, datas de início e término das atividades envolvidas no processo.
Já no que diz respeito à verificação de processos de workflow mapeados em Diagramas
de Atividades da UML, a principal vantagem desta abordagem é a transformação de
um modelo semi-formal em um modelo formal, para o qual algumas propriedades, como
soundness, podem ser formalmente verificadas. / Mestre em Ciência da Computação
| Identifer | oai:union.ndltd.org:IBICT/urn:repox.ist.utl.pt:RI_UFU:oai:repositorio.ufu.br:123456789/12473 |
| Date | 27 May 2009 |
| Creators | Passos, Lígia Maria Soares |
| Contributors | Maia, Marcelo de Almeida, Julia, Stéphane, Lopes, Carlos Roberto, 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/masterThesis |
| 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.0064 seconds