Resumo: O gerenciamento de workflows é uma realidade atualmente, mas os sistemas atuais carecem de suporte à verificação de correção em modelos de workflow. Este trabalho visa a realização de verificações em processos, objetivando a detecção de erros sintáticos, como a existência de atividades mal modeladas, ou seja, sem condições de entrada ou de saída. É objetivo deste trabalho também a definição de verificações de ordem estrutural, como detectar se o processo de workflow não possui deadlocks (estado em que o processo trava sem possibilidade de progredir), ou verificar se existem atividades mortas no processo (atividades impossíveis de serem executadas), ou se há terminações incompletas, ou seja, transições pendentes após o processo ter atingido seus objetivos. Além de verificações sintáticas e estruturais, é necessário também a realização de verificações semânticas do modelo, ou seja, é importante que os processos possam ser validados quanto a características que dizem respeito à sua organização lógica, a um nível um pouco mais alto de informação do que simplesmente estrutural. Por exemplo, é diretamente impactante na qualidade do modelo de um processo, definir se este possui conflitos ao acesso de recursos. Dessa forma, um processo estruturalmente correto, pode ficar travado em um deadlock, devido à concorrência quanto ao acesso de um recurso comum entre atividades distintas. Além disso, verificações de restrições de custo, por exemplo, também podem inviabilizar um processo. Todas essas verificações são importantes para decidir se um processo de workflow é correto. A maior contribuição deste trabalho, é então a definição de uma modelagem de processos de workflow que possibilite a verificação de problemas sintáticos, estruturais e semânticos, todos em uma única ferramenta, que se mostra escalável para processos reais, além de possibilitar a verificação de questões ad-hoc, específicas de cada instância, como verificar ordenações entre atividades específicas, etc Ver menos

Abstract: Workflow management is a reality nowadays, but today's systems give very little support to verify correctness in workflow models. This work aims to perform formal verification, with the goal of detecting syntactic errors, like the existence of activities poorly modeled, in other words, activities with no precondition or effect. It is a goal too, the definition of workflows structural verification, as to detect if the process does not have deadlocks (state in which the process is stuck with no possibility of getting any further), or verifying if there are dead activities in the process (activities impossible to be reached), or if exist incomplete terminations, ie, pending transitions after the process reached its objectives. Besides syntactic and structural verifications, it is necessary too, to perform semantic verifications in the process, in other words, it is important to validate the processes in respect to characteristics of its logical organization, in a higher level of information than simply structural verification. For example, it is directly impacting in the quality of the process model the definition if it has resource access conflicts. In this way, a process that is structurally correct, can be stuck in a deadlock, due to the concurrency in the access of a common resource of distinct activities. Besides that, verifications of costs restrictions, for example, can spoil a process. All these verifications are important to decide if a workflow model is correct. The main contribution of this work is the definition of workflow processes modeling that makes it possible to perform syntactic, structural and semantic verifications, all in a unique tool, that is showed to be scalable for real process, and even possible to verify ad-hoc questions, specific to the model, as checking activities ordering, for example Ver menos