The modeling and evaluation calculus FMC-QE, the Fundamental Modeling Concepts for Quanti-tative Evaluation [1], extends the Fundamental Modeling Concepts (FMC) for performance modeling and prediction. In this new methodology, the hierarchical service requests are in the main focus, because they are the origin of every service provisioning process. Similar to physics, these service requests are a tuple of value and unit, which enables hierarchical service request transformations at the hierarchical borders and therefore the hierarchical modeling. Through reducing the model complexity of the models by decomposing the system in different hierarchical views, the distinction between operational and control states and the calculation of the performance values on the assumption of the steady state, FMC-QE has a scalable applica-bility on complex systems. According to FMC, the system is modeled in a 3-dimensional hierarchical representation space, where system performance parameters are described in three arbitrarily fine-grained hierarchi-cal bipartite diagrams. The hierarchical service request structures are modeled in Entity Relationship Diagrams. The static server structures, divided into logical and real servers, are de-scribed as Block Diagrams. The dynamic behavior and the control structures are specified as Petri Nets, more precisely Colored Time Augmented Petri Nets. From the structures and pa-rameters of the performance model, a hierarchical set of equations is derived. The calculation of the performance values is done on the assumption of stationary processes and is based on fundamental laws of the performance analysis: Little's Law and the Forced Traffic Flow Law. Little's Law is used within the different hierarchical levels (horizontal) and the Forced Traffic Flow Law is the key to the dependencies among the hierarchical levels (vertical). This calculation is suitable for complex models and allows a fast (re-)calculation of different performance scenarios in order to support development and configuration decisions. Within the Research Group Zorn at the Hasso Plattner Institute, the work is embedded in a broader research in the development of FMC-QE. While this work is concentrated on the theoretical background, description and definition of the methodology as well as the extension and validation of the applicability, other topics are in the development of an FMC-QE modeling and evaluation tool and the usage of FMC-QE in the design of an adaptive transport layer in order to fulfill Quality of Service and Service Level Agreements in volatile service based environments. This thesis contains a state-of-the-art, the description of FMC-QE as well as extensions of FMC-QE in representative general models and case studies. In the state-of-the-art part of the thesis in chapter 2, an overview on existing Queueing Theory and Time Augmented Petri Net models and other quantitative modeling and evaluation languages and methodologies is given. Also other hierarchical quantitative modeling frameworks will be considered. The description of FMC-QE in chapter 3 consists of a summary of the foundations of FMC-QE, basic definitions, the graphical notations, the FMC-QE Calculus and the modeling of open queueing networks as an introductory example. The extensions of FMC-QE in chapter 4 consist of the integration of the summation method in order to support the handling of closed networks and the modeling of multiclass and semaphore scenarios. Furthermore, FMC-QE is compared to other performance modeling and evaluation approaches. In the case study part in chapter 5, proof-of-concept examples, like the modeling of a service based search portal, a service based SAP NetWeaver application and the Axis2 Web service framework will be provided. Finally, conclusions are given by a summary of contributions and an outlook on future work in chapter 6. [1] Werner Zorn. FMC-QE - A New Approach in Quantitative Modeling. In Hamid R. Arabnia, editor, Procee-dings of the International Conference on Modeling, Simulation and Visualization Methods (MSV 2007) within WorldComp ’07, pages 280 – 287, Las Vegas, NV, USA, June 2007. CSREA Press. ISBN 1-60132-029-9. / FMC-QE (Fundamental Modeling Concepts for Quantitative Evaluation [1]) ist eine auf FMC, den Fundamental Modeling Concepts, basierende Methodik zur Modellierung des Leistungsverhaltens von Systemen mit einem dazugehörenden Kalkül zur Erstellung von Leistungsvorhersagen wie Antwortzeiten und Durchsatz. In dieser neuen Methodik steht die Modellierung der hierarchischen Bedienanforderungen im Mittelpunkt, da sie der Ursprung aller dienstbasierenden Systeme sind. Wie in der Physik sind in FMC-QE die Bedienanforderungen Tupel aus Wert und Einheit, um Auftragstransformationen an Hierarchiegrenzen zu ermöglichen. Da die Komplexität durch eine Dekomposition in mehreren Sichten und in verschiedene hierarchische Schichten, die Unterscheidung von Operations- und Kontrollzuständen, sowie dazugehörige Berechungen unter Annahme der Stationarität reduziert wird, skaliert die Anwendbarkeit von FMC-QE auf komplexe Systeme. Gemäß FMC wird das zu modellierende System in einem 3-dimensionalen hierarchischen Beschreibungsraum dargestellt. Die quantitativen Kenngrößen der Systeme werden in drei beliebig frei-granularen hierarchischen bi-partiten Graphen beschrieben. Die hierarchische Struktur der Bedienanforderungen wird in Entity Relationship Diagrammen beschrieben. Die statischen Bedienerstrukturen, unterteilt in logische und reale Bediener, sind in Aufbaudiagrammen erläutert. Außerdem werden Petri Netze, genauer Farbige Zeit-behaftete Petri Netze, dazu verwendet, die dynamischen Abläufe, sowie die Kontrollflüsse im System zu beschreiben. Anschließend wird eine Menge von hierarchischen Gleichungen von der Struktur und den Parametern des Modells abgeleitet. Diese Gleichungen, die auf dem stationären Zustand des Systems beruhen, basieren auf den beiden Fundamental Gesetzen der Leistungsanalyse, dem Gesetz von Little und dem Verkehrsflussgesetz. Das Gesetz von Little definiert hierbei Beziehungen innerhalb einer hierarchischen Schicht (horizontal) und das Verkehrsflussgesetz wiederum Beziehungen zwischen hierarchischen Schichten (vertikal). Die Berechungen erlauben Leistungsvorhersagen für komplexe Systeme durch eine effiziente Berechnung von Leistungsgrößen für eine große Auswahl von System- und Lastkonfigurationen. Innerhalb der Forschungsgruppe von Prof. Dr.-Ing Werner Zorn am Hasso Plattner Institut an der Universität Potsdam ist die vorliegende Arbeit in einen größeren Forschungskontext im Bereich FMC-QE eingebettet. Während hier ein Fokus auf dem theoretischen Hintergrund, der Beschreibung und der Definition der Methodik als auch der Anwendbarkeit und Erweiterung gelegt wurde, sind andere Arbeiten auf dem Gebiet der Entwicklung einer Anwendung zur Modellierung und Evaluierung von Systemen mit FMC-QE bzw. der Verwendung von FMC-QE zur Entwicklung einer adaptiven Transportschicht zur Einhaltung von Dienstgüten (Quality of Service) und Dienstvereinbarungen (Service Level Agreements) in volatilen dienstbasierten Systemen beheimatet. Diese Arbeit umfasst einen Einblick in den Stand der Technik, die Beschreibung von FMC-QE sowie die Weiterentwicklung von FMC-QE in repräsentativen allgemeinen Modellen und Fallstudien. Das Kapitel 2: Stand der Technik gibt einen Überblick über die Warteschlangentheorie, Zeit-behaftete Petri Netze, weitere Leistungsbeschreibungs- und Leistungsvorhersagungstechniken sowie die Verwendung von Hierarchien in Leistungsbeschreibungstechniken. Die Beschreibung von FMC-QE in Kapitel 3 enthält die Erläuterung der Grundlagen von FMC-QE, die Beschreibung einiger Grundannahmen, der graphischen Notation, dem mathematischen Modell und einem erläuternden Beispiel. In Kapitel 4: Erweiterungen von FMC-QE wird die Behandlung weiterer allgemeiner Modelle, wie die Modellklasse von geschlossenen Netzen, Synchronisierung und Mehrklassen-Modelle beschrieben. Außerdem wird FMC-QE mit dem Stand der Technik verglichen. In Kapitel 5 werden Machbarkeitsstudien beschrieben. Schließlich werden in Kapitel 6 eine Zusammenfassung und ein Ausblick gegeben. [1] Werner Zorn. FMC-QE - A New Approach in Quantitative Modeling. In Hamid R. Arabnia, editor, Proceedings of the International Conference on Modeling, Simulation and Visualization Methods (MSV 2007) within WorldComp ’07, 280 – 287, Las Vegas, NV, USA, Juni 2007. CSREA Press. ISBN 1-60132-029-9.

In recent years there has been an exponential growth in Internet traffic resulting in increased network bandwidth requirements which, in turn, has led to stringent processing requirements on network layer devices like routers. Present backbone routers on OC 48 links (2.5Gbps) have to process four million minimum-sized packets per second. Further, the functionality supported in the network devices is also on the increase leading to programmable processors, such as Intel's IXP, Motorola's C5 and IBM's.NP. These processors support multiple processors and multiple threads to exploit packet-level-parallelism inherent in network workloads. This thesis studies the performance of network processors. We develop a Petri Net model for a commercial network processors (Intel IXP 2400,2850) for three different applications viz., IPv4 forwarding, Network Address Translation and IP security protocols. A salient feature of the Petri net model is its ability to model the application, architecture and their interaction in great detail. The model is validated using the intel proprietary tool (SDK 3.51 for IXP architecture) over a range of configurations. Our Performance evaluation results indicate that 1. The IXP processor is able to support a throughput of 2.5 Gbps for all modeled applications. 2. Packet buffer memory (DRAM) is the bottleneck resource in a network proces sor and even multithreading is ineffective beyond a total of 16 threads in case of header processing applications and beyond 32 threads for payload processing applications. Since DRAM is the bottleneck resource we explore the benefits of increasing the DRAM banks and other software schemes like offloading the packet header to SRAM. The second part of the thesis studies the impact of parallel processing in network processor on packet reordering and retransmission. Our results indicate that the concurrent processing of packets in a network processor and buffer allocation schemes in TFIFO leads to a significant packet reordering, (61%), on a 10-hop network (with packet sizes of 64 B) which in turn leads to a 76% retransmission under the TCP fast-restransmission algorithm. We explore different transmit buffer allocation schemes namely, contiguous, strided, local, and global for transmit buffer which reduces the packet retransmission to 24%. Our performance results also indicate that limiting the number of microengines can reduce the extent of packet reordering while providing the same throughput. We propose an alternative scheme, Packetsort, which guarantees complete packet ordering while achieving a throughput of 2.5 Gbps. Further, we observe that Packetsort outperforms, by up to 35%, the in-built schemes in the IXP processor namely, Inter Thread Signaling (ITS) and Asynchronous Insert and Synchronous Remove (AISR). The final part of this thesis investigates the performance of the network processor in a bursty traffic scenario. We model bursty traffic using a Pareto distribution. We consider a parallel and pipelined buffering schemes and their impact on packet drop under bursty traffic. Our results indicate that the pipelined buffering scheme outperforms the parallel scheme.

The major problem addressed in this thesis is the definition of a new SPLE methodology that covers both phases of the SPLE process and focuses on the derivation of behavioral models of SPL products. In Chapter 2 three research areas scope context of this thesis: Software Product Lines, Business Processes, and Model-Driven Engineering. Throughout Chapter 3, we propose a new SPLE methodology that focuses on the derivation of product behavior. We first describe the main flow of the methodology, and then detail the individual steps. In chapter 4 we propose a new domain specific language called CBPF created for modeling composable business process fragments. A model driven approach is followed for creating CBPF: definition of the abstract syntax, graphical concrete syntax and translational semantics. In Chapter 5 we propose several types of verifications that can be applied to business processfragments to determine their "correctness". For structural verification we definine a set of fragment consistency rules that should be valid for every business process fragment created with CBPF. To check behavioral correctness we first transform the business process fragment into an equivalent HCPN. We can then check generic properties but also define aset of fragment specific properties. In chapter 6 we exemplify the proposed SPL methodology by applying it to a case study from the crisis management system domain. We also propose a tool suite that supports our methodology. Chapter 7 describes possible improvements and extensions to the contributions of this thesis. We conclude the thesis in Chapter 8 and draw some conclusions.

This work is devoted to the issue of monitoring of distributed real-time systems. In particular, it focuses on formal aspects of model-based supervision and problems which are related to it. In its first part, we present the basic properties of two well-known formal models used to model distributed systems: networks of timed automata and time Petri nets. We show that the behavior of these models can be represented with so-called branching processes. We also introduce the key conceptual elements of the supervisory system. The second part of the work is dedicated to the issue of constrained unfoldings which enable us to track causal relationships between events in a distributed system. This type of structure can be used to reproduce processes of the system on the basis of a completely unordered set of previously observed events. Moreover, we show that time constraints imposed on a system and observations submitted to the supervisory system can significantly affect a course of events in the system. We also raise the issue of parameters in time constraints. The proposed methods are illustrated with case studies. The third part of the work deals with the issue of unobservable cyclical behaviors in distributed systems. This type of behaviors leads to an infinite number of events in constrained unfoldings. We explain how we can obtain a finite structure that stores information about all observed events in the system, even if this involves processes that are infinite due to such unobservable loops. The fourth and final part of the work is dedicated to implementation issues of the previously described methods.

In order to generate substantial market impact, mobile applications must be able to run on multiple platforms. Hence, software engineers face a multitude of technologies and system versions resulting in static variability. Furthermore, due to the dependence on sensors and connectivity, mobile software has to adapt its behavior accordingly at runtime resulting in dynamic variability. However, software engineers need to assure quality of a mobile application even with this large amount of variability—in our approach by the use of model-based testing (i.e., the generation of test cases from models). Recent concepts of test metamodels cannot efficiently handle dynamic variability. To overcome this problem, we propose a process for creating black-box test models based on dynamic feature Petri nets, which allow the description of configuration-dependent behavior and reconfiguration. We use feature models to define variability in the system under test. Furthermore, we illustrate our approach by introducing an example translator application.

Companies strive to improve their business processes in order to remain competitive. Process mining aims to infer meaningful insights from process-related data and attracted the attention of practitioners, tool-vendors, and researchers in recent years. Traditionally, event logs are assumed to describe the as-is situation. But this is not necessarily the case in environments where logging may be compromised due to manual logging. For example, hospital staff may need to manually enter information regarding the patient’s treatment. As a result, events or timestamps may be missing or incorrect. In this paper, we make use of process knowledge captured in process models, and provide a method to repair missing events in the logs. This way, we facilitate analysis of incomplete logs. We realize the repair by combining stochastic Petri nets, alignments, and Bayesian networks. We evaluate the results using both synthetic data and real event data from a Dutch hospital. / Unternehmen optimieren ihre Geschäftsprozesse laufend um im kompetitiven Umfeld zu bestehen. Das Ziel von Process Mining ist es, bedeutende Erkenntnisse aus prozessrelevanten Daten zu extrahieren. In den letzten Jahren sorgte Process Mining bei Experten, Werkzeugherstellern und Forschern zunehmend für Aufsehen. Traditionell wird dabei angenommen, dass Ereignisprotokolle die tatsächliche Ist-Situation widerspiegeln. Dies ist jedoch nicht unbedingt der Fall, wenn prozessrelevante Ereignisse manuell erfasst werden. Ein Beispiel hierfür findet sich im Krankenhaus, in dem das Personal Behandlungen meist manuell dokumentiert. Vergessene oder fehlerhafte Einträge in Ereignisprotokollen sind in solchen Fällen nicht auszuschließen. In diesem technischen Bericht wird eine Methode vorgestellt, die das Wissen aus Prozessmodellen und historischen Daten nutzt um fehlende Einträge in Ereignisprotokollen zu reparieren. Somit wird die Analyse unvollständiger Ereignisprotokolle erleichtert. Die Reparatur erfolgt mit einer Kombination aus stochastischen Petri Netzen, Alignments und Bayes'schen Netzen. Die Ergebnisse werden mit synthetischen Daten und echten Daten eines holländischen Krankenhauses evaluiert.

Petri nets are a simple formalism for modelling concurrent computation. This formalism has been proposed as a promising tool to describe and analyse biochemical networks. In this thesis, we explore the structural properties of Petri nets as a mean to provide information about the biochemical system evolution and its dynamics, especially when kinetic data are missing, making simulations impossible. In particular, we consider the structural properties of siphons and traps. We show that these structures entail a family of particular stability properties which can be characterized by a fragment of CTL over infinite state structures. Mixed integer linear programs have been proposed and a state-of-the-art algorithm from the Petri net community has been described later to compute minimal sets of siphons and traps in Petri nets. We present a simple boolean model capturing these notions and compare SAT and CLP methods for enumerating the set of all minimal siphons and traps of a Petri net. Our methods are applied to a benchmark composed of the 403 models from the biomodels.net repository. We analyse why these programs perform so well on even very large biological models. We show that, in networks with bounded tree-width, the existence of a minimal siphon containing a given set of places can be decided in a linear time, and the Siphon-Trap property as well. Moreover, we consider two other Petri net structural properties: place and transition invariants. We present a simple method to extract minimal semi-positive invariants of a Petri net as a constraint satisfaction problem on finite domains using constraint programming with symmetry detection and breaking. This allows us to generalize well-known results about the steady-state analysis of symbolic Ordinary Differential Equations systems corresponding to biochemical reactions by taking into account the structure of the reaction network. The study of the underlying Petri net, initially introduced for metabolic flux analysis, provides classes of reaction systems for which the symbolic computation of steady states is possible.

Workflow systems aim to provide automated support for the conduct of certain business processes. Workflow systems are driven by workflow specifications which among others, capture the execution interdependencies between various activities. These interdependencies are modelled by means of different control flow constructors, e.g., sequence, choice, parallelism and synchronisation. It has been shown in the research on workflow patterns that the support for and the interpretation of various control flow constructs varies substantially across workflow systems. Two of the most problematic patterns relate to the OR-join and to cancellation. An OR-join is used in situations when we need to model " wait and see" behaviour for synchronisation. Different approaches assign a different (often only intuitive) semantics to this type of join, though they do share the common theme that synchronisation is only to be performed for active paths. Depending on context assumptions this behaviour may be relatively easy to deal with, though in general its semantics is complicated, both from a definition point of view (in terms of formally capturing a desired intuitive semantics) and from a computational point of view (how does one determine whether an OR-join is enabled?). Many systems and languages struggle with the semantics and implementation of the OR-join because its non-local semantics require a synchronisation depending on an analysis of future execution paths. This may require some non-trivial reasoning. The presence of cancellation features and other OR-joins in a workflow further complicates the formal semantics of the OR-join. The cancellation feature is commonly used to model external events that can change the behaviour of a running workflow. It can be used to either disable activities in certain parts of a workflow or to stop currently running activities. Even though it is possible to cancel activities in workflow systems using some sort of abort function, many workflow systems do not provide direct support for this feature in the workflow language. Sometimes, cancellation affects only a selected part of a workflow and other activities can continue after performing a cancellation action. As cancellation occurs naturally in business scenarios, comprehensive support in a workflow language is desirable. We take on the challenge of providing formal semantics, verification techniques as well as an implementation for workflows with those features. This thesis addresses three interrelated issues for workflows with cancellation regions and OR-joins. The concept of the OR-join is examined in detail in the context of the workflow language YAWL, a powerful workflow language designed to support a collection of workflow patterns and inspired by Petri nets. The OR-join semantics has been redesigned to represent a general, formal, and decidable approach for workflows in the presence of cancellation regions and other OR-joins. This approach exploits a link that is proposed between YAWL and reset nets, a variant of Petri nets with a special type of arc that can remove all tokens from a place. Next, we explore verification techniques for workflows with cancellation regions and OR-joins. Four structural properties have been identified and a verification approach that exploits coverability and reachability notions from reset nets has been proposed. The work on verification techniques has highlighted potential problems with calculating state spaces for large workflows. Applying reduction rules before carrying out verification can decrease the size of the problem by cutting down the size of the workflow that needs to be examined while preserving some essential properties. Therefore, we have extended the work on verification by proposing reduction rules for reset nets and for YAWL nets with and without OR-joins. The proposed OR-join semantics as well as the proposed verification approach have been implemented in the YAWL environment.

Over the past decade, the ubiquity of business processes and their need for ongoing management in the same manner as other corporate assets has been recognized through the establishment of a dedicated research area: Business Process Management (or BPM). There are a wide range of potential software technologies on which a BPM o®ering can be founded. Although there is signi¯cant variation between these alternatives, they all share one common factor { their execution occurs on the basis of a business process model { and consequently, this ¯eld of technologies can be termed Process-Aware Information Systems (or PAIS). This thesis develops a conceptual foundation for PAIS based on the results of a detailed examination of contemporary o®erings including work°ow and case han- dling systems, business process modelling languages and web service composition languages. This foundation is based on 126 patterns that identify recurrent core constructs in the control-°ow, data and resource perspectives of PAIS. These patterns have been used to evaluate some of the leading systems and business process modelling languages. It also proposes a generic graphical language for de¯ning exception handling strategies that span these perspectives. On the basis of these insights, a comprehensive reference language { newYAWL { is developed for business process modelling and enactment. This language is formally de¯ned and an abstract syntax and operational semantics are provided for it. An assessment of its capabilities is provided through a comprehensive patterns-based analysis which allows direct comparison of its functionality with other PAIS. newYAWL serves as a reference language and many of the ideas embodied within it are also applicable to existing languages and systems. The ultimate goal of both the patterns and newYAWL is to improve the support and applicability of PAIS.

Denial-of-service attacks (DoS) and distributed denial-of-service attacks (DDoS) attempt to temporarily disrupt users or computer resources to cause service un- availability to legitimate users in the internetworking system. The most common type of DoS attack occurs when adversaries °ood a large amount of bogus data to interfere or disrupt the service on the server. The attack can be either a single-source attack, which originates at only one host, or a multi-source attack, in which multiple hosts coordinate to °ood a large number of packets to the server. Cryptographic mechanisms in authentication schemes are an example ap- proach to help the server to validate malicious tra±c. Since authentication in key establishment protocols requires the veri¯er to spend some resources before successfully detecting the bogus messages, adversaries might be able to exploit this °aw to mount an attack to overwhelm the server resources. The attacker is able to perform this kind of attack because many key establishment protocols incorporate strong authentication at the beginning phase before they can iden- tify the attacks. This is an example of DoS threats in most key establishment protocols because they have been implemented to support con¯dentiality and data integrity, but do not carefully consider other security objectives, such as availability. The main objective of this research is to design denial-of-service resistant mechanisms in key establishment protocols. In particular, we focus on the design of cryptographic protocols related to key establishment protocols that implement client puzzles to protect the server against resource exhaustion attacks. Another objective is to extend formal analysis techniques to include DoS- resistance. Basically, the formal analysis approach is used not only to analyse and verify the security of a cryptographic scheme carefully but also to help in the design stage of new protocols with a high level of security guarantee. In this research, we focus on an analysis technique of Meadows' cost-based framework, and we implement DoS-resistant model using Coloured Petri Nets. Meadows' cost-based framework is directly proposed to assess denial-of-service vulnerabil- ities in the cryptographic protocols using mathematical proof, while Coloured Petri Nets is used to model and verify the communication protocols using inter- active simulations. In addition, Coloured Petri Nets are able to help the protocol designer to clarify and reduce some inconsistency of the protocol speci¯cation. Therefore, the second objective of this research is to explore vulnerabilities in existing DoS-resistant protocols, as well as extend a formal analysis approach to our new framework for improving DoS-resistance and evaluating the performance of the new proposed mechanism. In summary, the speci¯c outcomes of this research include following results; 1. A taxonomy of denial-of-service resistant strategies and techniques used in key establishment protocols; 2. A critical analysis of existing DoS-resistant key exchange and key estab- lishment protocols; 3. An implementation of Meadows's cost-based framework using Coloured Petri Nets for modelling and evaluating DoS-resistant protocols; and 4. A development of new e±cient and practical DoS-resistant mechanisms to improve the resistance to denial-of-service attacks in key establishment protocols.