La technologie de workflow, tendant à automatiser les processus d'entreprise et à fournir un support pour leur gestion, est aujourd'hui un secteur actif de recherche. C'est dans ce contexte que se situent ces travaux de thèse qui portent aussi bien sur la modélisation des processus workflow que sur leur vérification. Ces processus, pouvant être contraints par des ressources partagées ou encore par des durées de traitement, doivent être vérifiés avant d'être confiés aux systèmes de gestion de workflow qui vont les exécuter. Nous nous sommes intéressés par la vérification de la propriété de cohérence (soundness) des réseaux de workflow (WF-net) : sous-classes des réseaux de Petri (RdPs) modélisant les processus workflow.Dans ce cadre, en explorant la théorie structurelle des RdPs, nous avons identifié des sous-classes de WF-nets pour lesquelles la cohérence peut être vérifiée et caractérisée efficacement. Nous nous sommes focalisés en outre sur l'extension de ces sous-classes en tenant compte de la présence de ressources partagées et sur la propriété de cohérence en présence d'un nombre arbitraire d'instances prêtes à s'exécuter. Dans cette partie, nous avons dû automatiser le calcul des siphons minimaux dans un RdP. Pour ce faire, nous avons choisi un algorithme de la littérature et l'amélioré par la recherche et la contraction de circuits alternés.Ensuite, nous avons abordé la modélisation et la vérification de processus workflow tenant compte des contraintes temporelles. Nous avons en premier lieu proposé un modèle de TWF-net (WF-net Temporisé). Pour ce modèle, nous avons défini la propriété de cohérence temporelle et proposé une condition nécessaire et suffisante pour la vérifier. En deuxième lieu, nous avons relaxé les contraintes temporelles adoptées par la proposition d'un modèle temporel visant des processus à contraintes temporelles variant dans des intervalles de temps. Nous avons défini formellement le modèle de ITWF-net (Interval Timed WF-net) et donné sa sémantique. Par ailleurs, nous avons développé et testé un prototype de modélisation et de simulation des ITWF-nets.La dernière partie de cette thèse a concerné la vérification formelle des processus workflow par SPIN model checker. Nous avons dû en premier lieu traduire la spécification des workflows adoptée vers Promela : le langage de description des modèles à vérifier par SPIN. En second lieu, nous avons exprimé les propriétés de cohérence en Logique Linéaire Temporelle (LTL) et utilisé SPIN pour tester si chaque propriété est satisfaite par le modèle Promela du WF-net en question. Enfin, nous avons exprimé les propriétés de k-cohérence pour les WF-nets modélisant plusieurs instances et de (k,R)-cohérence pour les processus workflow concurrents et qui possèdent des ressources partagées. / Workflow technology, whose role is to automate business processes and to provide a support for their management, is today an active sector of research. This thesis deals with the modelling of the workflow processes and their analysis. These processes, probably constrained by shared resources or by durations of treatment, must be checked before being executed by their workflow management systems. In this direction, we were interested by the checking of the soundness property of workflow nets (WF-nets): subclasses of Petri nets modelling the workflow processes.To begin with, by exploring the structure theory of Petri nets, we have identified subclasses of WF-nets for which soundness can be checked and characterized effectively. We also extended these subclasses by taking account of the presence of shared resources and we focused on the soundness property in the presence of an arbitrary number of instances ready to be carried out. In this part, we had to automate the computation of minimal siphons in a Petri net. For that, we chose an algorithm of the literature and improved it by the research and the contraction of alternate circuits.Then, we were concerned by the modelling and the analysis of workflow processes holding temporal constraints. We initially proposed the model of TWF-net (Timed WF-net). For this model, we defined its soundness and proposed a method to check it. Then, we released the adopted temporal constraints by the proposal of a model covering workflow processes for witch temporal constraints vary in time intervals. We formally defined the model of ITWF-net (Interval Timed WF-net) and gave its semantics. In addition, we developed and tested a prototype of modelling and simulation of ITWF-nets.The last part of this thesis concerns the formal analysis of workflow processes with SPIN model checker. We initially translated the workflow specification into Promela: the model description language used by SPIN. Then, we expressed the soundness properties in Linear Temporal Logic (LTL) and used SPIN to test if each property is satisfied by the Promela model of a given WF-net. Moreover, we expressed the properties of k-soundness for WF-nets modelling several instances and (k,R)-soundness for competitive workflow processes which share resources.

A well-structured and coordinated information management practice is central to promoting efficiency in construction. Building information management encompasses authoring, interpretation, communication, coordination and storage of building information. The benefits envisioned by utilizing IT developments such as Building Information Modelling (BIM) in the facility management and operations (FM&amp;O) sector are estimated to be far greater than in other sectors. There is, however, a gap between the knowledge available in the field of building information management and the actual demands of the architectural, engineering, construction and operation (AECO) industry, especially the FM&amp;O sector. The overall aim of this qualitative research is to develop knowledge that conceptualizes the lifecycle supporting implementation of BIM in the AECO industry with a focus on its implications for a BIM-enabled FM&amp;O practice. This applied research comprises a number of summative and formative components: paper 1 investigates the existing and emerging information management systems for the FM&amp;O sector and their characteristics. The focus of paper 2 is narrowed down to the technical requirements on building information management systems; while its temporal scope spans the entire lifecycle of buildings. Paper 3 is a further elaboration on the findings of paper 1 and covers the technical requirements of BIM-implementation in the FM&amp;O sector. Paper 4 investigates workflows – another category of the issues identified in paper 1. Paper 1 aims to provide a general understanding of the importance and implications of implementing BIM-enabled systems in the FM&amp;O sector and also identifies the main categories of the issues associated with this approach. This literary paper reports on a basic research with a descriptive approach and builds upon the information from a non-exhaustive set of literature. In this paper, workflows, contracts and information technology have been identified as three categories of the issues associated with implementing BIM-enabled systems in the FM&amp;O sector. Paper 2 is also a literary research which draws on the notion of BIM repositories and aims to clarify the technical requirements for a more collaborative building industry as well as depicting the current status of building knowledge management technologies, recent trends and future prospects. Open format BIM repositories have been suggested as the cornerstones of an integrated information management system for AECO firms. The aim of paper 3 is twofold: firstly, to summarize the current status of the building information management technologies applied in the facility operation activities and identifying prevailing issues; secondly, to devise some technical solutions for those issues based on a case project. In the first part of this study, a summarized description of information management configurations in eleven projects were extracted from literature and the technical issues within those systems were identified. Moreover, five major categories of contemporary technical solutions for enhancing information transfer from BIM to FM&amp;O software were designated. Then, a narrative and illustrative representation and reconstruction of an IT-implementation project was developed. Paper 4 is another literary study which aims to provide the theoretical basis for more focused studies on existing and desired processes in the FM&amp;O sector and their associated information transactions. In this paper, firstly, the more common definitions of the key concepts have been revisited and discussed. Then, the generic types of the processes, activities and organizational roles common to FM&amp;O firms, the types of information required by each actor and how such information are acquired have been presented. / <p>QC 20150423</p>

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

The thesis deals with workflow design and its implementation in a construction company. The current state of document management is becoming obsolete and insufficient. Thus the company´s board has approved the realization of workflow system. The aim of this thesis is therefore analysis of company´s related processes and design of a workflow model. In addition, the new model is required to be linked with present financial and managerial accounting systems and allow for future adjustments and modifications. Final output of this thesis consists of workflow process maps, risk assessment, budget and time plan of realization.