Process modelling is a design approach where a system or procedure is decomposed in a number of abstract, independent, but connected processes, and then recomposed into a well-defined workflow specification. Research in formal verification, for its part, and theorem proving in particular, is focused on the rigorous verification of system properties using logical proof. This thesis introduces a systematic methodology for process modelling and composition based on formal verification. Our aim is to augment the numerous benefits of a workflow based specification, such as modularity, separation of concerns, interoperability between heterogeneous (including human-based) components, and optimisation, with the high level of trust provided by formally verified properties, such as type correctness, systematic resource accounting (including exception handling), and deadlock-freedom. More specifically, we focus on bridging the gap between the deeply theoretical proofs-as-processes paradigm and the highly pragmatic tasks of process specification and composition. To accomplish this, we embed the proofs-as-processes paradigm within the modern proof assistant HOL Light. This allows the formal, mechanical translation of Classical Linear Logic (CLL) proofs to p-calculus processes. Our methodology then relies on the specification of abstract processes in CLL terms and their composition using CLL inference. A fully diagrammatic interface is used to guide our developed set of high level, semi-automated reasoning tools, and to perform intuitive composition actions including sequential, parallel, and conditional composition. The end result is a p-calculus specification of the constructed workflow, with guarantees of correctness for the aforementioned properties. We can then apply a visual, step-by-step simulation of this workflow or perform an automated workflow deployment as executable code in the programming language Scala. We apply our methodology to a use-case of a holiday booking web agent and to the modelling of real-world collaboration patterns in healthcare, thus demonstrating the capabilities of our framework and its potential use in a variety of scenarios.

The final thesis is focused on the topic of process management and its development in time. Business Process Management and workflow, are described in the thesis as well as its specification and classification. The paper compares these two concepts. The thesis also works with the methodology of ARIS and Balanced Scorecard which are applied in the selected process of the organization. The process is built on the BPMN notation which is also described in the thesis. The aim of the thesis is to examine and to analyze selected process of the organization with specific methodology, to specify potential problems in the process and to suggest possible solution.

Organizações modernas apresentam demandas relacionadas à automação dos seus processos de negócio devido à alta complexidade dos mesmos e à necessidade de maior eficácia na execução. Neste contexto, a tecnologia de workflow tem se mostrado bastante eficiente, principalmente para a automatização dos processos de negócio. No entanto, por ser uma tecnologia emergente e em evolução, workflow apresenta algumas limitações. Ainda que diversos (meta) modelos de workflow tenham sido propostos nos últimos, anos, seus sub-modelos para representação dos aspectos estruturais da organização apresentam baixo poder de expressão. Além disso, a maioria das ferramentas para modelagem de workflow não provêm funcionalidades para definição, consulta e reuso de padrões. Um dos principais problemas é falta de um mapeamento consolidado entre padrões de funções recorrentes em processos de negócio (ex: solicitação de execução de atividade, aprovação de documentos) e (meta) modelos e/ou ferramentas para modelagem de processos de negócio e workflow. Além disso, a maioria das abordagens em padrões de workflow não exploram a completude e necessidade dos seus padrões para modelagem de workflow. A primeira contribuição desta tese é um Modelo Transacional de Processos de Negócio (MTPN) com suporte aos aspectos estruturais da organização. O metamodelo possibilita a criação de (sub-)processos de negócio a partir do reuso de padrões, principalmente com base nestes aspectos. Adicionalmente, o metamodelo sugere a geração automática de padrões através da Linguagem de Execução para Web Services (BPEL4WS). Outra importante contribuição da tese é um conjunto de padrões de workflow representados como atividades de bloco. Cada padrão descreve uma função recorrente em processos de negócio. A mineração de 190 processos de workflow de mais de 10 organizações diferentes provou a existência dos padrões com alto suporte nos processos de workflow analisados. Além disso, o estudo mostrou que o conjunto de padrões é suficiente e necessário para modelar todos os 190 processos investigados. O estudo também resultou em um conjunto de regras de associação. As regras não apenas contribuem para uma melhor definição dos padrões de atividade de bloco, mas também para a combinação destes com padrões de controle de fluxo. / Modern organizations have demands related to the automation of their business processes since such processes are highly complex and need to be efficiently executed. Within this context, the workflow technology has shown to be very effective, mainly in the business process automation. However, as it is an emergent technology and in constant evolution, workflow presents some limitations. Though several workflow (meta) models have been proposed in recent years, their sub-models for organizational structure aspects representation show limited power of expression. On the other hand, most of the current workflow modeling tools do not provide functionalities that enable users to define, query, and reuse workflow patterns properly. One of the main problems is the non-availability of a consolidated mapping between patterns based on recurrent functions found in business processes (e.g., request for activity execution, notification, decision, or approval) and workflow (meta) models or workflow modeling tools. Relying on these problems, the first contribution of this thesis is a Transactional Metamodel of Business Process (TMBP) with support to organizational structure aspects. The metamodel makes feasible to create business (sub-)processes from the reuse of organizational –based workflow patterns. An additional feature of TMBP supports the generation of business (sub-)processes through the Business Process Execution Language for Web Services (BPEL4WS). Other important contribution of this thesis is a set of workflow patterns represented as block activity patterns. Each pattern refers to a recurrent business function frequently found in business processes. The mining of 190 workflow processes of more than 10 different organizations has evidenced the existence of the set of workflow patterns with high support in the workflow processes analyzed. Moreover, it became clear through this study that the set of patterns is both necessary and enough to design all 190 processes that were investigated. As a consequence of the mining process, a set of association rules was identified too. The rules not only help to better define specific workflow patterns, but also combine them with existent control flow patterns. These rules can be useful for building more complex workflows.

Organizações modernas apresentam demandas relacionadas à automação dos seus processos de negócio devido à alta complexidade dos mesmos e à necessidade de maior eficácia na execução. Neste contexto, a tecnologia de workflow tem se mostrado bastante eficiente, principalmente para a automatização dos processos de negócio. No entanto, por ser uma tecnologia emergente e em evolução, workflow apresenta algumas limitações. Ainda que diversos (meta) modelos de workflow tenham sido propostos nos últimos, anos, seus sub-modelos para representação dos aspectos estruturais da organização apresentam baixo poder de expressão. Além disso, a maioria das ferramentas para modelagem de workflow não provêm funcionalidades para definição, consulta e reuso de padrões. Um dos principais problemas é falta de um mapeamento consolidado entre padrões de funções recorrentes em processos de negócio (ex: solicitação de execução de atividade, aprovação de documentos) e (meta) modelos e/ou ferramentas para modelagem de processos de negócio e workflow. Além disso, a maioria das abordagens em padrões de workflow não exploram a completude e necessidade dos seus padrões para modelagem de workflow. A primeira contribuição desta tese é um Modelo Transacional de Processos de Negócio (MTPN) com suporte aos aspectos estruturais da organização. O metamodelo possibilita a criação de (sub-)processos de negócio a partir do reuso de padrões, principalmente com base nestes aspectos. Adicionalmente, o metamodelo sugere a geração automática de padrões através da Linguagem de Execução para Web Services (BPEL4WS). Outra importante contribuição da tese é um conjunto de padrões de workflow representados como atividades de bloco. Cada padrão descreve uma função recorrente em processos de negócio. A mineração de 190 processos de workflow de mais de 10 organizações diferentes provou a existência dos padrões com alto suporte nos processos de workflow analisados. Além disso, o estudo mostrou que o conjunto de padrões é suficiente e necessário para modelar todos os 190 processos investigados. O estudo também resultou em um conjunto de regras de associação. As regras não apenas contribuem para uma melhor definição dos padrões de atividade de bloco, mas também para a combinação destes com padrões de controle de fluxo. / Modern organizations have demands related to the automation of their business processes since such processes are highly complex and need to be efficiently executed. Within this context, the workflow technology has shown to be very effective, mainly in the business process automation. However, as it is an emergent technology and in constant evolution, workflow presents some limitations. Though several workflow (meta) models have been proposed in recent years, their sub-models for organizational structure aspects representation show limited power of expression. On the other hand, most of the current workflow modeling tools do not provide functionalities that enable users to define, query, and reuse workflow patterns properly. One of the main problems is the non-availability of a consolidated mapping between patterns based on recurrent functions found in business processes (e.g., request for activity execution, notification, decision, or approval) and workflow (meta) models or workflow modeling tools. Relying on these problems, the first contribution of this thesis is a Transactional Metamodel of Business Process (TMBP) with support to organizational structure aspects. The metamodel makes feasible to create business (sub-)processes from the reuse of organizational –based workflow patterns. An additional feature of TMBP supports the generation of business (sub-)processes through the Business Process Execution Language for Web Services (BPEL4WS). Other important contribution of this thesis is a set of workflow patterns represented as block activity patterns. Each pattern refers to a recurrent business function frequently found in business processes. The mining of 190 workflow processes of more than 10 different organizations has evidenced the existence of the set of workflow patterns with high support in the workflow processes analyzed. Moreover, it became clear through this study that the set of patterns is both necessary and enough to design all 190 processes that were investigated. As a consequence of the mining process, a set of association rules was identified too. The rules not only help to better define specific workflow patterns, but also combine them with existent control flow patterns. These rules can be useful for building more complex workflows.

Organizações modernas apresentam demandas relacionadas à automação dos seus processos de negócio devido à alta complexidade dos mesmos e à necessidade de maior eficácia na execução. Neste contexto, a tecnologia de workflow tem se mostrado bastante eficiente, principalmente para a automatização dos processos de negócio. No entanto, por ser uma tecnologia emergente e em evolução, workflow apresenta algumas limitações. Ainda que diversos (meta) modelos de workflow tenham sido propostos nos últimos, anos, seus sub-modelos para representação dos aspectos estruturais da organização apresentam baixo poder de expressão. Além disso, a maioria das ferramentas para modelagem de workflow não provêm funcionalidades para definição, consulta e reuso de padrões. Um dos principais problemas é falta de um mapeamento consolidado entre padrões de funções recorrentes em processos de negócio (ex: solicitação de execução de atividade, aprovação de documentos) e (meta) modelos e/ou ferramentas para modelagem de processos de negócio e workflow. Além disso, a maioria das abordagens em padrões de workflow não exploram a completude e necessidade dos seus padrões para modelagem de workflow. A primeira contribuição desta tese é um Modelo Transacional de Processos de Negócio (MTPN) com suporte aos aspectos estruturais da organização. O metamodelo possibilita a criação de (sub-)processos de negócio a partir do reuso de padrões, principalmente com base nestes aspectos. Adicionalmente, o metamodelo sugere a geração automática de padrões através da Linguagem de Execução para Web Services (BPEL4WS). Outra importante contribuição da tese é um conjunto de padrões de workflow representados como atividades de bloco. Cada padrão descreve uma função recorrente em processos de negócio. A mineração de 190 processos de workflow de mais de 10 organizações diferentes provou a existência dos padrões com alto suporte nos processos de workflow analisados. Além disso, o estudo mostrou que o conjunto de padrões é suficiente e necessário para modelar todos os 190 processos investigados. O estudo também resultou em um conjunto de regras de associação. As regras não apenas contribuem para uma melhor definição dos padrões de atividade de bloco, mas também para a combinação destes com padrões de controle de fluxo. / Modern organizations have demands related to the automation of their business processes since such processes are highly complex and need to be efficiently executed. Within this context, the workflow technology has shown to be very effective, mainly in the business process automation. However, as it is an emergent technology and in constant evolution, workflow presents some limitations. Though several workflow (meta) models have been proposed in recent years, their sub-models for organizational structure aspects representation show limited power of expression. On the other hand, most of the current workflow modeling tools do not provide functionalities that enable users to define, query, and reuse workflow patterns properly. One of the main problems is the non-availability of a consolidated mapping between patterns based on recurrent functions found in business processes (e.g., request for activity execution, notification, decision, or approval) and workflow (meta) models or workflow modeling tools. Relying on these problems, the first contribution of this thesis is a Transactional Metamodel of Business Process (TMBP) with support to organizational structure aspects. The metamodel makes feasible to create business (sub-)processes from the reuse of organizational –based workflow patterns. An additional feature of TMBP supports the generation of business (sub-)processes through the Business Process Execution Language for Web Services (BPEL4WS). Other important contribution of this thesis is a set of workflow patterns represented as block activity patterns. Each pattern refers to a recurrent business function frequently found in business processes. The mining of 190 workflow processes of more than 10 different organizations has evidenced the existence of the set of workflow patterns with high support in the workflow processes analyzed. Moreover, it became clear through this study that the set of patterns is both necessary and enough to design all 190 processes that were investigated. As a consequence of the mining process, a set of association rules was identified too. The rules not only help to better define specific workflow patterns, but also combine them with existent control flow patterns. These rules can be useful for building more complex workflows.

The main objective of this thesis is to make an analysis and to design of a system for the support of distant management staff. An emphasis is placed upon the system design for effective utilization in practice and openness for further development. The theoretical part is divided into three main chapters. The first chapter is about describing the issues of process and project management in terms of the focus of this thesis. The output of this chapter is a list of the general requirements of the system for the support of distant management staff. In the second chapter is an analysis of the market with systems that best meet the defined general requirements. The third chapter is about describing the methods which are used in the practical part of this thesis. The practical part is mainly about realizing the main objective of this thesis. The practical part is divided into three main chapters. The first chapter contains a catalog of requirements for the system for support remote management staff. The second chapter is describing the design of the requirements defined in the first chapter of practical part. The last chapter of this thesis contains a comparison of the designed system and other systems of a similar type.

This thesis deals with an optimalization of the Escalation process in the customer support department in the company Centrum služeb s.r.o. It contains the analysis of the current process and theoretical knowledge to propose a new solution. The proposed solution is a website based application, which automates the process and decreases the time to resolve customers requests.

Today, business process modelling is important part of analysis and design of the information systems. There is number of standards, which is concerned with process modelling, whereas each of them represents a little different approach. The project Opensoul created general metamodel, which defines basic elements and their mutual associations, which all standards should meet. In other words, it defines basic rules for process modelling. The goal of this thesis is to compare chosen standards of process modelling with Business process metamodel of Opensoul initiative. The results of this comparison would have provide basis to answer the question, which standard supports in the best way the rules of process modelling defined by metamodel through the system of elements and their associations. This goal requires specifying the method, on which basis the comparison will be made. This method comprises the extension of metamodel with new elements and their relations to other elements, and the extension of some elements with some workflow patterns defined by Workflow Patterns initiative. That is the main benefit of this thesis.

The master’s thesis is concerning the field of process management and workflow in company 2Tom s.r.o. Theoretical part of the thesis presents actual trends of management and methods of increasing process effectiveness, the thesis analyses actual state of the company and presents proposals for implementation and usage of workflow oriented on the key processes of the company.

Im CoolSoftware-Projekt wurden Metamodelle, Algorithmen und Architekturmuster für energieeffiziente Software entworfen. Sobald ein komplexer Kontrollfluss auf einem solchen System ausgeführt werden soll, muss das dynamische Energieverhalten in die Optimierung einbezogen werden. Um diese Herausforderung zu lösen, werden in dieser Arbeit die Ansätze von CoolSoftware durch weitere Modellelemente und Algorithmen ergänzt. Unter anderem kommt eine Simulation zum Einsatz, um funktionell mögliche Konfigurationen zu bewerten. Der Kontrollfluss kann durch das Workflow-Management-System Open Service Process Platform definiert werden. Im Ergebnis kann das System den Workflow je nach Komplexität möglichst energiearm ausführen.