This diploma thesis deals with digital libraries of Czech regional libraries. Based on the available sources of the literature and the questionnaire survey, digital libraries, which are built by regional libraries, are introduced. At the beginning of the thesis is a terminological overview, together with digitization and digitization workflow itself. Then follows a description of the personal layout in digital libraries as well as various activities and standards of digital libraries. The thesis is supplemented by a description of the individual Czech digital libraries, which are built by regional libraries. The thesis also contains the results of a questionnaire survey among regional libraries and outlines the problem areas of regional digital libraries.

This diploma thesis is devoted to digital libraries of Czech regional libraries. Based on the available sources of literature and the questionnaire survey, the individual digital libraries that are built and administered by regional libraries are presented. In the first chapters of the thesis there is a terminological overview, the process of digitization itself and the digitization workflow. This is followed by a description of the distribution of personal representation of individual positions in digital libraries as well as the standards of digital libraries. An important part of the thesis is devoted to the results of the questionnaire survey among individual regional libraries and the presentation of the results of this survey. At the end of the thesis, the problem areas of regional digital libraries are outlined. Keywords digital library, regional library, workflow, digitization, staffing, standards

The correctness of a workflow specification is critical for the automation of business processes. For this reason, errors in the specification should be detected and corrected as early as possible - at specification time. In this paper, we present a validation method for workflow specifications using model-checking techniques. A formalized workflow specification, its properties and the correctness requirements are translated into a timed state machine that can be analyzed with the Uppaal model checker. The main contribution of this paper is the use of timed model checking for verifying time-related properties of workflow specifications. Using only one tool (the model checker) for verifying these different kinds of properties gives an advantage over using different specialized algorithms for verifying different kinds of properties.

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.

Der Chirurg in einem modernen Operationssaal kann auf die Funktionen einer Vielzahl technischer, seine Arbeit unterstützender, Geräte zugreifen. Diese Geräte und damit auch die Funktionen, die diese zur Verfügung stellen, sind nur unzureichend miteinander vernetzt. Die unzureichende Interoperabilität der Geräte bezieht sich dabei nicht nur auf den Austausch von Daten untereinander, sondern auch auf das Fehlen eines zentralen Wissens über den gesamten Ablauf des chirurgischen Prozesses. Es werden daher Systeme benötigt, die Prozessmodelle verarbeiten und damit globales Wissen über den Prozess zur Verfügung stellen können. Im Gegensatz zu den meisten Prozessen, die in der Wirtschaft durch Workflow Management-Systeme (WfMS) unterstützt werden, ist der chirurgische Prozess durch eine hohe Variabilität gekennzeichnet. Mittlerweile gibt es viele Ansätze feingranulare, hochformalisierte Modelle des chirurgischen Prozesses zu erstellen. In dieser Arbeit wird zum einen die Qualität eines, auf patienten individuellen Eingriffen basierenden, generalisierten Modells hinsichtlich der Abarbeitung durch ein WfMS untersucht, zum anderen werden die Voraussetzungen die, die vorgelagerten Systeme erfüllen müssen geprüft. Es wird eine Aussage zur Abbruchrate der Pfadverfolgung im generalisierten Modell gemacht, das durch eine unterschiedliche Anzahl von patientenindividuellen Modellen erstellt wurde. Zudem wird die Erfolgsrate zum Wiederfinden des Prozesspfades im Modell ermittelt. Ausserdem werden die Anzahl der benötigten Schritte zumWiederfinden des Prozesspfades im Modell betrachtet.:List of Figures iv List of Tables vi 1 Introduction 1 1.1 Motivation 1 1.2 Problems and objectives 3 2 State of research 6 2.1 Definitions of terms 6 2.1.1 Surgical process 6 2.1.2 Surgical Process Model 7 2.1.3 gSPM and surgical workflow 7 2.1.4 Surgical workflow management system 8 2.1.5 Summary 9 2.2 Workflow Management Systems 10 2.2.1 Agfa HealthCare - ORBIS 10 2.2.2 Siemens Clinical Solutions - Soarian 10 2.2.3 Karl Storz - ORchestrion 10 2.2.4 YAWL BPM 11 2.3 Sensor systems 12 2.3.1 Sensors according to DIN1319 13 2.3.2 Video-based sensor technology 14 2.3.3 Human-based sensor technology 15 2.3.4 Summary 15 2.4 Process model 15 2.4.1 Top-Down 15 2.4.2 Bottom-Up 17 2.4.3 Summary 18 2.5 Methods for creating the ICCAS process model 18 2.5.1 Recording of the iSPMs 18 2.5.2 Creation of the gSPMs 20 2.6 Summary 21 3 Model-based design of workflow schemas 23 3.1 Abstract 24 3.2 Introduction 25 3.3 Model driven design of surgical workflow schemata 27 3.3.1 Recording of patient individual surgical process models 27 3.3.2 Generating generalized SPM from iSPMs 27 3.3.3 Transforming gSPM into workflow schemata 28 3.4 Summary and Outlook 30 4 Model-based validation of workflow schemas 31 4.1 Abstract 32 4.2 Introduction 33 4.3 Methods 36 4.3.1 Surgical Process Modeling 36 4.3.2 Workflow Schema Generation 38 4.3.3 The SurgicalWorkflow Management and Simulation System 40 4.3.4 System Validation Study Design 42 4.4 Results 44 4.5 Discussion 47 4.6 Conclusion 50 4.7 Acknowledgments 51 5 Influence of missing sensor information 52 5.1 Abstract 53 5.2 Introduction 54 5.3 Methodology 57 5.3.1 Surgical process modeling 57 5.3.2 Test system 59 5.3.3 System evaluation study design 61 5.4 Results 63 5.5 Discussion 66 5.6 Conclusion 68 5.7 Acknowledgments 68 5.8 Conflict of interest 68 6 Summary and outlook 69 6.1 Summary 69 6.2 Outlook 70 Bibliography 74

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.

In recent years, the Internet of Things (IoT) has increasingly received attention from the Business Process Management (BPM) community. The integration of sensors and actuators into Process-Aware Information Systems (PAIS) enables the collection of real-time data about physical properties and the direct manipulation of real-world objects. In a broader sense, IoT-aware workflows provide means for context-aware workflow execution involving virtual and physical entities. However, IoT-aware workflow management imposes new requirements on workflow modeling and execution that are outside the scope of current modeling languages and workflow management systems. Things in the IoT may vanish, appear or stay unknown during workflow execution, which renders their allocation as workflow resources infeasible at design time. Besides, capabilities of Things are often intended to be available only in a particular real-world context at runtime, e.g., a service robot inside a smart home should only operate at full speed, if there are no residents in direct proximity. Such contextual restrictions for the dynamic exposure of resource capabilities are not considered by current approaches in IoT resource management that use services for exposing device functionalities. With this work, we aim at providing the modeling and runtime support for defining such restrictions on workflow resources at design time and enabling the dynamic and context-sensitive runtime allocation of Things as workflow resources. To achieve this goal, we propose contributions to the fields of resource management, i.e., resource perspective, and workflow management in the Internet of Things (IoT), divided into the user perspective representing the workflow modeling phase and the workflow perspective representing the runtime resource allocation phase. In the resource perspective, we propose an ontology for the modeling of Things, Roles, capabilities, physical entities, and their context-sensitive interrelations. The concept of Role is used to define non-exclusive subsets of capabilities of Things. A Thing can play a certain Role only under certain contextual restrictions defined by Semantic Web Rule Language (SWRL) rules. At runtime, the existing relations between the individuals of the ontology represent the current state of interactions between the physical and the cyber world. Through the dynamic activation and deactivation of Roles at runtime, the behavior of a Thing can be adapted to the current physical context. In the user perspective, we allow workflow modelers to define the goal of a workflow activity either by using semantic queries or by specifying high-level goals from a Tropos goal model. The goal-based modeling of workflow activities provides the most flexibility regarding the resource allocation as several leaf goals may fulfill the user specified activity goal. Furthermore, the goal model can include additional Quality of Service (QoS) parameters and the positive or negative contribution of goals towards these parameters. The workflow perspective includes the Semantic Access Layer (SAL) middleware to enable the transformation of activity goals into semantic queries as well as their execution on the ontology for role-based Things. The SAL enables the discovery of fitting Things, their allocation as workflow resources, the invocation of referenced IoT services, and the continuous monitoring of the allocated Things as part of the ontology. We show the feasibility and added value of this work in relation to related approaches by evaluation within several application scenarios in a smart home setting. We compare the fulfillment of quantified criteria for IoT-aware workflow management based on requirements extracted from related research. The evaluation shows, that our approach enables an increase in the context-aware modeling of Things as workflow resources, in the query support for workflow resource allocation, and in the modeling support of activities using Things as workflow resources.:1 Introduction 15 1.1 Background 17 1.2 Motivation 17 1.3 Aim and Objective 19 1.3.1 Research Questions and Scope 19 1.3.2 Research Goals 20 1.4 Contribution 20 1.5 Outline 21 2 Background for Workflows in the IoT 23 2.1 Resource Perspective 24 2.1.1 Internet of Things 24 2.1.2 Context and Role Modeling 27 2.2 User Perspective 37 2.2.1 Goal Modeling 38 2.2.2 Tropos Goal Modeling Language 38 2.3 Workflow Perspective 39 2.3.1 Workflow Concepts 39 2.3.2 Workflow Modeling 40 2.3.3 Internet of Things-aware Workflow Management 43 2.4 Summary 44 3 Requirements Analysis and Approach 45 3.1 Requirements 45 3.1.1 IoT Resource Perspective 46 3.1.2 Workflow Resource Perspective 50 3.1.3 Relation to Research Questions 51 3.2 State of the Art Analysis 53 3.2.1 Fulfillment Criteria 54 3.2.2 IoT-aware workflow management 56 3.3 Discussion 65 3.4 Approach 70 3.4.1 Contribution to IoT-aware workflow management 71 3.5 Summary 73 4 Concept for Adaptive Workflow Activities in the IoT 75 4.1 Resource Perspective 75 4.1.1 Role-based Things 75 4.1.2 Semantic Modeling Concepts 79 4.1.3 SWRL Modeling Concepts 81 4.2 User Perspective 81 4.2.1 Semantic Queries in Workflow Activites 81 4.2.2 Goals for Workflow Activites 81 4.2.3 Mapping from Goals to Semantic Queries 82 4.3 Workflow Perspective 83 4.3.1 Workflow metamodel Extensions 83 4.3.2 Middleware for Dynamic Resource Discovery and Allocation 85 4.4 Summary 86 5 Modeling Adaptive Workflow Activities in the IoT 87 5.1 Resource Perspective 87 5.1.1 Role-based Modeling of Context-sensitive Things 87 5.1.2 Ontology Classes 90 5.1.3 Ontology Object properties 93 5.1.4 Ontology Data properties 99 5.1.5 DL-safe SWRL Rules 100 5.2 Discussion of Role Modeling Features 101 5.3 Example Application Scenario Modeling 102 5.3.1 Resource Perspective 102 5.3.2 User Perspective 105 5.3.3 Workflow Perspective 109 5.4 Summary 113 6 Architecture for Adaptive Workflow Activities in the IoT 115 6.1 Overview of the System Architecture 115 6.2 Specification of System Components 117 6.2.1 Resource Perspective 118 6.2.2 User Perspective 118 6.2.3 Workflow Perspective 118 6.3 Summary 123 7 Implementation of Adaptive Workflow Activities in the IoT 125 7.1 Resource Perspective 125 7.2 Workflow Perspective 125 7.2.1 PROtEUS 125 7.2.2 Semantic Access Layer 127 7.3 User Perspective 128 7.4 Summary 128 8 Evaluation 129 8.1 Goal and Evaluation Approach 129 8.1.1 Definition of Test Cases 130 8.2 Scenario Evaluation 134 8.2.1 Ambient Assisted Living Setting 135 8.2.2 Resource Perspective 135 8.2.3 User Perspective 137 8.2.4 Workflow Perspective 138 8.2.5 Execution of Test Cases 139 8.2.6 Discussion of Results 146 8.3 Performance Evaluation 148 8.3.1 Experimental Setup 148 8.3.2 Discussion of Results 151 8.4 Summary 152 9 Discussion 153 9.1 Comparison of Solution to Research Questions 153 9.2 Extendability of the Solutions 155 9.3 Limitations 156 10 Summary and Future Work 157 10.1 Summary of the Thesis 157 10.2 Future Work 159 Appendix 161 Example Semantic Context Model for IoT-Things 171 T-Box of Ontology for Role-based Things in the IoT 178 A-Box for Example Scenario Model 201 A-Box for Extended Example Scenario Model 210

A system safety assurance case aims to demonstrate that a system is reasonably safe within the parameters defined according to its intended use. A system safety assurance case involves the definition of a Safety Engineering Process and its execution for the particular system. An essential element in the Safety Engineering Process is hazard analysis. An often used version of hazard analysis is HAZOP. HAZOP identifies hazards and hazardous events in the system's design. Traditionally, HAZOP is performed based on the expertise of a multi-disciplinary team. This team uses a heuristic based approach that results in documented output that often does not include adequate traceability as to how the output results were obtained. This thesis proposes a systematic approach to HAZOP that was developed after performing detailed analysis on how traditional HAZOP is performed in industry. It aims to produce documented output in which the output results are traceable to interim steps in the process. We call this systematic approach HAZOP+, because it was designed to provide sufficient detail so that it can form the basis of a HAZOP metamodel created in Workflow+ - a relatively new model driven methodology for developing assurance cases. Workflow+ has well-defined semantics, and so we refer to HAZOP+ as formalizable. HAZOP+ has a number of benefits over traditional HAZOP, and these benefits are demonstrated by comparing a traditional application of HAZOP with the application of HAZOP+, both applied to a typical Lane Keeping Assist feature. A long term objective of system safety assurance is to be able to perform incremental safety assurance, for example, by updating the system safety assurance case after a modification to the system or its environment. Since the safety assurance case for a system depends on elements of the Safety Engineering Process, as well as the outputs of that process, the ability to perform an incremental hazard analysis after a modification to the system or environment can be a real benefit. This thesis further describes how HAZOP+ can be enhanced/extended to HAZOPdelta - an incremental version of HAZOP+. / Thesis / Master of Applied Science (MASc)

Den här studien fokuserar på att undersöka workflow hos musikproducenter för att kunna identifiera konkreta tips som förbättrar effektivitet och hantverk i musikskapande. Genom kvalitativa intervjuer med sex erfarna musikproducenter i Berlin och en i Stockholm har en lista med tio konkreta tips för att förbättra sitt workflow skapats. Resultaten visar bland annat att balansera effektivitet mot hantverk utefter produktionens / låtens ändamål är nyckeln till ett bra workflow. För att validera tipsens effektivitet skapades tre musikproduktioner som var väldigt olika varandra, där tipsen testades. Efter att de konstnärliga verken var färdiga analyserades valet av workflow och arbetsmetoder till dessa produktioner för att bedöma påverkan på musikens uttryck och sound. / This study focuses on investigating the workflow of music producers in order to identify concrete tips that improve efficiency and craftsmanship in music creation. Through qualitative interviews with six experienced music producers in Berlin and one in Stockholm, a list of ten tips to improve your workflow has been created. The results show that balancing efficiency with craftsmanship according to the purpose of the production/song is the key to a good workflow. To validate the effectiveness of the tips, three very different music productions were created, where the tips were tested. After the artistic works were completed, the choice of workflow and working methods for these productions was analyzed to assess the impact on the expression and sound of the music.

<p>Objectives: (1) to assess whether computer simulation modeling or process modeling have improved medication management systems, including informing the design of e-prescribing systems for Canada, and (2) to build and validate a workflow diagram of the handwritten medication management process in the community setting for Canada and use it to obtain feedback from stakeholders.</p> <p>Methods: A systematic review was conducted to assess whether the modeling techniques have improved medication management systems. A workflow diagram was developed and used to obtain feedback from stakeholders as to where problems exist in the current paper-based process and where information technology might be of help. Analyses were descriptive and qualitative.</p> <p>Results: The systematic review identified 13,376 citations, 8 of which were included in the full data extraction. The review revealed that simulation models of e-prescribing systems have been developed, but their accuracy and usefulness has not been established. One process model had been used to analyze a Canadian medication management system, but no evidence was found that process models had any positive impact on e-prescribing development in Canada.</p> <p>Fifteen stakeholders, including 5 physicians, 5 pharmacists, and 5 members of the public provided feedback using the workflow diagram. All stakeholders agreed that the diagram was a realistic representation of the actual handwritten medication management process, suggesting face validity. The majority of stakeholders identified the most problematic processes as generating the prescription by the physician (9/15 (60.0%)) and drug checking by the physician (6/15 (40.0%)).</p> <p>Conclusions: There is a lack of published evidence on simulation models and process models, and the studies that exist do not suggest any benefit in informing e-prescribing design. We developed and established face validity for a workflow diagram of the paper-based medication management cascade. Stakeholders believed that generating the prescription and drug checking by the physician could be improved by e-prescribing.</p> / Master of Science (MSc)