Please use this identifier to cite or link to this item: https://repositorio.ufu.br/handle/123456789/12473
Full metadata record
DC FieldValueLanguage
dc.creatorPassos, Lígia Maria Soares
dc.date.accessioned2016-06-22T18:32:14Z-
dc.date.available2009-07-21
dc.date.available2016-06-22T18:32:14Z-
dc.date.issued2009-05-27
dc.identifier.citationPASSOS, Lígia Maria Soares. Formalização de workflow nets utilizando lógica linear: análise qualitativa e quantitativa. 2009. 104 f. Dissertação (Mestrado em Ciências Exatas e da Terra) - Universidade Federal de Uberlândia, Uberlândia, 2009.por
dc.identifier.urihttps://repositorio.ufu.br/handle/123456789/12473-
dc.description.abstractThis 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.eng
dc.description.sponsorshipCoordenação de Aperfeiçoamento de Pessoal de Nível Superior
dc.formatapplication/pdfpor
dc.languageporpor
dc.publisherUniversidade Federal de Uberlândiapor
dc.rightsAcesso Abertopor
dc.subjectProcessos de workflowpor
dc.subjectLógica linearpor
dc.subjectPlanejamento de recursospor
dc.subjectDiagrama de atividades da umlpor
dc.subjectAtlpor
dc.subjectWorkflow processeng
dc.subjectWorkflow nets, Soundnesseng
dc.subjectLinear logiceng
dc.subjectResource planningeng
dc.subjectUml activity diagramseng
dc.subjectEngenharia de softwarepor
dc.subjectFluxo de trabalhopor
dc.titleFormalização de workflow nets utilizando lógica linear: análise qualitativa e quantitativapor
dc.typeDissertaçãopor
dc.contributor.advisor-co1Maia, Marcelo de Almeida
dc.contributor.advisor-co1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4791753E8por
dc.contributor.advisor1Julia, Stéphane
dc.contributor.advisor1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4796960H1por
dc.contributor.referee1Lopes, Carlos Roberto
dc.contributor.referee1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4788535Z4por
dc.contributor.referee2Villani, Emilia
dc.contributor.referee2Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4769237U2por
dc.creator.Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4485036H6por
dc.description.degreenameMestre em Ciência da Computaçãopor
dc.description.resumoEste 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.por
dc.publisher.countryBRpor
dc.publisher.programPrograma de Pós-graduação em Ciência da Computaçãopor
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAOpor
dc.publisher.departmentCiências Exatas e da Terrapor
dc.publisher.initialsUFUpor
Appears in Collections:DISSERTAÇÃO - Ciência da Computação

Files in This Item:
File Description SizeFormat 
Ligia.pdf949.41 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.