This thesis describes opinions about generating code from PNtalk language into more standard object orinted languages, such as C++ or Java. Goal is to construct model of the formalism of Object Oriented Petri Nets (OOPN), represented in PNtalk languege in mentioned languages. This model should be simlpier and more effective than actual implementation in Smalltalk language. Thesis also contains ideas about abstactization the code generator to be able to generate code in various languages.

Thesis focuses on interpretation of nested petri nets described in PNML language on Atmel processors. It introduces this limited - from memory capacity and perfomance point of views - targeted architecture, since it greatly affected both design and implementation. The interpreter is thouroughly described from all aspects of its design. One of most important concerns in the whole process was the ability to test and verify achieved state of functionality quickly and possibly without Atmel processor. That’s why the implentation took place on a squeak platform, that allowed to translate whole interpreter for targeted platform. Motivation behind this and overall process of translation is also a subject of this work.

This project pursues issues on the border of information technologies and process optimization. Previously published concepts of~modeling projects and shared resources with object-oriented Petri nets are presented and further expanded. The possibilites of~the use of~genetic algorithms for dynamic realtime optimization of the resource schedules are explored. The resource constrained project sheduling problem is presented and it is shown, how instances of the problem can be implemented. A more complex model that is inspired by real production systems is then created. Next, a control agent, which monitors a running production system and allows for it's dynamic optimization is designed. The whole system is implemented in the Squeak Smalltalk environment with the use of the tool PNtalk, which is an experimental implementation of the object oriented Petri nets paradigm.

Cette thèse porte sur le diagnostic des défauts dans des Systèmes à Evènements Discrets (SED) pour lesquels l’occurrence des événements est soumise à des contraintes temporelles. Les domaines d’application potentiels sont nombreux et variés allant de la production manufacturière aux systèmes de transport en passant par les réseaux de communication et les systèmes d’information. La complexité croissante de ces systèmes nécessite l’élaboration de méthodes de surveillance de plus en plus efficaces et performantes pour garantir leur sécurité, leur disponibilité ainsi que le maintien de leurs propriétés dans le temps. Les réseaux de Petri Stochastiques Temporisés Partiellement Observés (RdPSTPO) sont utilisés pour modéliser le système ainsi que les défauts qui peuvent l’affecter. L’étude concerne particulièrement les défauts qui se traduisent par la violation des contraintes temporelles. Une exploitation pertinente des informations temporelles, en vue du diagnostic, constitue la contribution majeure de la thèse. En effet, une meilleure utilisation de ces informations permet de discerner avec précision les différents comportements qui expliquent les mesures. De plus, la probabilité d’occurrence des défauts est calculée en fonction des dates des mesures collectées. Deux approches sont développées : la première est dédiée aux défauts ponctuels et la seconde aux dérives lentes dans les systèmes cycliques. / This PhD thesis deals with the fault diagnosis of Discrete Event Systems (DES) for which the occurrence of events is constrained by temporal specifications. The domain of application is large and varied ranging from manufacturing systems to transportation systems, communication networks and information systems. The increasing complexity of these systems requires the development of effective and efficient monitoring methods to ensure their security, availability and the maintenance of their properties over the time. For that purpose, Partially Observed Stochastic Timed Petri Nets (POSTPN) are used to model the system and the different faults that may affect it. The study is particularly concerned with faults that result after the violation of temporal constraints. Our main contribution in this thesis is the relevant exploitation of the timed information for the fault diagnosis. In fact, a better use of these temporal informations allow to discern with precision the different behaviors that are consistent with the measurements. In addition, the probability of faults occurrence is evaluated according to the dates of collected measurements. Two approaches are developed : the first one is used for single faults and the second one for slow drifts in cyclical systems.

Since the ability of Workforce Management Systems to handle mobility induced challenges of mobile environments like data-communication cut-offs, reduced network bandwidth, and security concerns improved recently, the optimization efforts of mobile enterprises increasingly focus on the organizational setup of their mobile environment. This includes issues like, e.g., the dimension and staffing of regional subdivisions, qualification balance of the workforce, and resource allocation strategies. While this multitude of possible adjustment parameters for optimization prevents from the analytical prediction of organizational change efforts, simulation is a promising approach to analyze mobile environments and their change. In this work we present a formal model representing a generalization of mobile environments. This model can be utilized to examine the cost situation and performance of both real mobile enterprises and projected future development scenarios of such enterprises. The model is developed using colored petri nets (CPN) and the software suite CPN Tools. We show that our model is capable of predicting the outcomes of organizational change projects by the utilization of simulation and present a validation of our model based on real-world data of a German gas and power supply.

This paper presents a class of Stochastic Petri Nets with concurrent transition firings. It is assumed that transitions occur in steps and that for every step each enabled transition decides probabilistically whether it wants to participate in the step or not. Among the transitions which what to participate in a step, a maximal number is chosen to perform the firing step. The observable behavior is defined and equivalence relations are introduced. The equivalence relations extend the well-known trace and bisimulation equivalences for systems with step semantics to Stochastik Petri Nets with concurrent transition firing. It is shown that the equivalence notions form a lattice of interrelations.

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.

Notre thèse est consacrée à l’étude de la supervision des réseaux de Petri en vue de la conception de systèmes manufacturiers flexibles. L’objectif est la définition de stratégies de pilotage en ligne pour l’évitement de conflits et d’interblocages, dans le cadre de la théorie de la supervision. Le point de départ de notre travail est d’exploiterle graphe de marquage du réseau de Petri, ce qui permet en particulier d’obtenir des stratégies de commande maximalement permissive pour des problèmes d’évitement de conflits et d’interblocages. Nous avons ainsi introduit des techniques originales, manipulations d’inégalités ou réductions d’ensembles de marquages, destinées à diminuerla complexité algorithmique d’une telle méthode. Dans premier temps, nous avons focalisé sur la synthèse de superviseurs dits purs, ce qui correspond au cas particulier où l’ensemble de marquage légaux, est convexe.Cette optimisation est ensuite considérée du point de vue de la facilité de mise en oeuvre. Nous traitons ainsi de la minimisation de la structure du superviseur et de son coût d’implémentation en préservant une structure de supervision qui offre à la fois la permissivité maximale et une complexité de calcul raisonnable en vue d’utilisationsur des installations réelles. Aussi, nous avons cherché à réduire le nombre de places de contrôle nécessaires pour réaliser un superviseur maximalement permissif, pour cela nous avons formule le calcul du nombre minimal de places de contrôle en termes d’un problème de programmation linéaire. Afin d’affaiblir la complexité de ce calcul de superviseur, deux versions de l’algorithme sont proposées. Ce problème de minimisation de la taille dusuperviseur, quoique fondamental, n’est pas abordé aussi directement dans la littérature. Il s’agit là d’une première contribution.Dans u second temps, nous nous sommes intéressés aux réseaux de Petri à boucles (self-loops). Les boucles étant représentées par une variable qui s’ajoute dans la contrainte inégalité définissant l’ensemble de marquages légaux. Après avoir proposé une méthode de réduction du nombre d’inégalités ainsi que du superviseur optimalen se basant sur les approches et résultats précédents, nous avons établi une condition suffisante d’obtention d’un superviseur maximalement permissif permettant de traiter des ensembles de marquages légaux non convexes.Enfin nous proposons une méthode de synthèse de contrôleur pour une nouvelle classe de réseaux de Petri, avec des arcs inhibiteurs correspondant à des contraintes définies par des intervalles. La taille du contrôleur ainsi obtenu et défini en termes d’arcs inhibiteurs à intervalles s’en trouve réduite ainsi que par conséquent sont coût d’implémentation. / Reachability graph analysis is an important technique for deadlockcontrol, which always suffers from a state explosion problem since it requires togenerate all or a part of reachable markings.Based on this technique, an optimal or suboptimal supervisor with high behavioralpermissiveness can always be achieved. This thesis focuses on designing liveness enforcing Petri net supervisors for FMSs by considering their behavioralpermissiveness, supervisory structure, and computationnal complexity.The following research contributions are made in this thesis.1. The design of a maximally permissive liveness-enforcing supervisor for an FMSis proposed by solving integer linear programming problems (ILPPs).2. Structural complexity is also an important issue for a maximally permissivePetri net supervisor. A deadlock prevention policy for FMSs is proposed, which canobtain a maximally permissive liveness-enforcing Petri net supervisor while thenumber of control places is compressed.3. In order to overcome the computational complexity problem in MCPP and ensurethat the controlled system is maximally permissive with a simple structure, wedevelop an iterative deadlock prevention policy and a modified version.4. We consider the hardware and software costs in the stage of controlimplementation of a deadlock prevention policy, aiming to obtain a maximallypermissive Petri net supervisor with the lowest implementation cost. A supervisorconsists of a set of control places and the arcs connecting control places totransitions. We assign an implementation cost for each control place and controland observation costs for each transition. Based on reachability graph analysis,maximal permissiveness can be achieved by designing place invariants that prohibitall FBMs but no legal markings.5. Self-loops are used to design maximally permissive supervisors. A self-loop ina Petri net cannot be mathematically represented by its incidence matrix. Wepresent a mathematical method to design a maximally permissive Petri netsupervisor that is expressed by a set of control places with self-loops. A controlplace with a self-loop can be represented by a constraint and a selfloopassociated with a transition whose firing may lead to an illegal marking.

For over a century, the railway system has been gradually designed and adapted to serve the corresponding demands under variations of given budgets. However, recent developments indicate that the railway systems of many European countries gradually come to their limits, as the national infrastructure managers declare an increasing share of their network tracks as congested. Consequently, the capabilities of each railway system are getting more into focus, to adequately serve the recent intention of shifting more demand to rail to encounter climate change. The system’s capacity is thereby of particular interest, i. e. whether the system already has the ability to serve increasing traffic loads by leveraging existing reserves, or otherwise needs significant extensions to serve the increasing demand. We thus need to quantify the current capacity of the railway system to identify its current capabilities and to deduct corresponding measures to leverage capacity reserves and relieve saturated network parts. Only the appropriate measure selection, i.e. deciding where to apply traffic reorganization and optimization or infrastructural extensions and restructuring, allows to achieve the goal of shifting more demand to rail under limited resource constraints. The main contributions of this thesis are in the design, optimization and application of a network capacity assessment approach for large-scale railway networks, which incorporates the perspectives of infrastructure, operations and demand by using the number of trains per time window and scheduled waiting times as capacity metric. Hence, this thesis provides a new definition of network capacity, and develops petri net (PN)-based capacity assessment models for railway networks with the use of mixed integer program (MIP) and row generation. The capacity is then determined by assessing the maximum utilization and the scheduled waiting times of the railway network with respect to infrastructure, railway operations and demand. We first introduce the definition of railway network capacity, which extends the concept of railway capacity from stations and corridors to entire networks. This new utilization-based and demand-centric definition of practical railway network capacity defines railway network capacity as the maximum number of departing trains in the network over a given time period, regarding the given infrastructure, operations and demand. This definition allows to accurately determine the interplay of infrastructure, operations and demand, with a combined measure of traffic flow and scheduled waiting times. In the context of this new definition on network capacity, different assessment approaches for the capacity of railway stations, corridors and networks are reviewed with regard to their spatial scope, the used approach and the applied capacity metric. Second we propose the railway network utilization model (RNUM), which extends an existing PN based approach from single line to entire network operations. This model builds upon individual lines, which are then connected to more complex structures. The analysis of the maximum utilization is based on the network’s elementary circuits. Furthermore, token modifications are introduced to characterize relevant process circuits and introduce interline separation places to model and assess complex networks. By additionally considering rolling stock circulations and imposed train orders, the utilization is determined for given operation scenarios of a line system, which operates at heterogeneous frequencies. The resulting timetable independent approach allows to fully characterize the utilization of the network. To assess the network capacity, an enumeration-based railway network capacity (RNC) framework is further introduced, which evaluates the maximum utilization over diverse operation scenarios to represent possible network demands. The resulting train flows as well as the average scheduled waiting times per train, the capacity and the corresponding network effects were finally quantified and determined in network-specific macroscopic fundamental diagram for the railway network (MFD-R). Third, we introduce the railway network utilization MIP model (MIP-RNUM) to determine the optimal capacity utilization by combining PNs with mathematical linear programming. The presented model is enabled to simultaneously assess different train locations and line orders to provide the network’s utilization, capacity-optimal train locations and line orders for given operation scenarios. The MIP-RNUM is further improved to provide the demand-centered capacity utilization, by incorporating extended demand structures, which capture the demanded flows and magnitudes as fixed proportions of trains per line. The additional incorporation of local routing and thus optimal line orders in the utilization assessment, extend the model further to provide the optimal and demand-centered capacity utilization without the correspondingly required enumeration of different line orders. The resulting fully extended MIP-RNUM comprehensively captures the interplay of infrastructure, railway operations and demand; and the resulting effects on the network capacity. Fourth, we propose the row generation MIP-RNUM (MIP-RNUM-RG) to assess the capacity of large-scale instances. The proposed approach tackles the computationally intensive enumeration of the network’s cycles of the RNUM by applying lazy-constraint generation i.e. iteratively adding violated constraints of previous solutions to the problem in a row generating manner. To assess the solution quality of intermediate solutions during the capacity assessment of large instances, a lower-bound method is presented, which combines a higher order max-plus system and a binary search algorithm. The lower-bound method allows to check the feasibility of a given solution and to quantify the optimality gap of the current results while solving the MIP-RNUM-RG. In summary, this thesis provides multiple scientific contributions to efficiently assess the capacity of complex railway networks by developing several assessment models and frameworks. By integrating the different perspectives of infrastructure, operations and demand, this thesis supports network design towards the development of demand-centric railway systems. Regarding the intended growth of the railway demand in the near future, this thesis can guide practitioners to assess the capabilities of our present railway systems and derive the necessary actions to transform them into the transport systems of our future. / Das Eisenbahnsystem wurde über ein Jahrhundert lang entworfen und angepasst, um die jeweilige Nachfrage unter einem sich verändernden Budget zu bedienen. Aktuelle Entwicklungen zeigen jedoch, dass die Eisenbahnsysteme vieler europäischer Länder allmählich an ihre Grenzen stoßen. Zeitgleich geraten die Fähigkeiten eines jeden Eisenbahnsystems in den Fokus, mit denen zur Begegnung des Klimawandels mehr Verkehr auf die Schiene verlagert werden kann. Die Systemkapazität ist dabei von besonderem Interesse, d. h. ob das System bereits in der Lage ist, wachsende Verkehrsmengen durch die Nutzung existierender Reserven zu bewältigen, oder ob es zur Bedienung der steigenden Nachfrage einen deutlichen Ausbau braucht. Aus diesem Grund muss die Kapazität des Eisenbahnsystems bewertet werden, um damit seine aktuellen Möglichkeiten zu identifizieren und durch entsprechend abgeleitete Maßnahmen Kapazitätsreserven nutzbar zu machen und saturierte Netzteile zu entlasten. Der wesentliche Beitrag dieser Arbeit liegt im Entwurf, der Erweiterung und Anwendung eines Ansatzes zur Untersuchung der Netzwerkkapazität für großräumige Eisenbahnnetze unter Einbeziehung der Einflussfaktoren Infrastruktur, Betrieb und Nachfrage. Als Kapazitätsmetrik kommen dabei die Zugzahlen pro Zeiteinheit und die planmäßigen Wartezeiten zum Einsatz. Diese Arbeit entwirft dafür eine neue Definition der Netzwerkkapazität und entwickelt anschließend Petri-Netz (PN) basierte Untersuchungsmodelle für die Eisenbahnnetzkapazität unter Nutzung von gemischt-ganzzahliger Programmierung und Zeilengenerierung (eng. row generation). Durch die Analyse der maximalen Kapazitätsausnutzung und der planmäßigen Wartezeiten im Netz wird die Kapazität unter Berücksichtigung der Einflussfaktoren bestimmt. Zuerst wird die Definition der Eisenbahnnetzwerkkapazität eingeführt, die das Konzept der Eisenbahnkapazität von Bahnhöfen und Streckenkorridoren auf Netzwerke erweitert. Diese neue, auf Kapazitätsausnutzung basierende, nachfragezentrierte Definition der praktischen Eisenbahnnetzwerkkapazität definiert die Netzkapazität als die maximale Anzahl der im Netzwerk abfahrenden Züge innerhalb eines gegebenen Zeitintervalls, unter Berücksichtigung der gegebenen Einflussfaktoren. Im Kontext dieser neuen Definition werden verschiedene, existierende Untersuchungsansätze für die Kapazität von Eisenbahnknoten, Streckenkorridoren und Netzwerken rezensiert. Die Ansätze werden insbesondere hinsichtlich ihres räumlichen Umfangs, des angewendeten Verfahrens und der jeweils genutzten Kapazitätsmetrik verglichen. Als Zweites wird das Eisenbahnnetzwerkausnutzungsmodell (eng. railway network utilization model – RNUM) präsentiert, das einen existierenden PN-Ansatz von einer einzelnen Linie auf Netzwerke erweitert. Dieses Modell setzt sich aus einzelnen Linien zusammen, die zu komplexeren Strukturen zusammengesetzt werden. Die Analyse der maximalen Kapazitätsausnutzung basiert auf den Elementarkreisen des entstehenden Netzwerks. Durch die zusätzliche Berücksichtigung von Fahrzeugumläufen und vorgegebenen Zugfolgen wird die Kapazitätsausnutzung für gegebene Betriebsszenarien eines Liniensystems bestimmt, in welchem die Linien mit heterogenen Taktzeiten verkehren. Der resultierende, fahrplanunabhängige Ansatz erlaubt die vollständige Charakterisierung der maximalen Kapazitätsausnutzung unter Berücksichtigung diverser Betriebsszenarien. Die resultierenden Zugverkehrsströme und die mittleren planmäßigen Wartezeiten pro Zug, die ermittelte Kapazität und die zugehörigen Netzwerkeffekte werden schließlich in einem netzwerkspezifischen makroskopischen Fundamentaldiagram für Eisenbahnnetzwerke (MFD-R) bestimmt. Als Drittes wird das Eisenbahnnetzwerkausnutzungs-MIP-modell (MIP-RNUM) eingeführt, um die optimale Kapazitätsausnutzung durch eine Kombination von PN und linearer Programmierung zu bestimmen. Das eingeführte Modell kann simultan verschiedene Zugpositionen und Zugfolgen berücksichtigen, um auf deren Grundlage die Netzwerkausnutzung, kapazitätsoptimale Zugpositionen und -folgen für gegebene Betriebsszenarien zu untersuchen. Im Folgenden wird das MIP-RNUM erweitert, um die nachfragezentrierte Kapazitätsausnutzung zu erfassen. Die zusätzliche Berücksichtigung von variablen Fahrwegen in Knoten und den zugehörigen optimalen Zugfolgen in der Ausnutzungsuntersuchung ergänzen das Modell zusätzlich, um die optimale und nachfragezentrierte Kapazitätsausnutzung ohne die bisher benötigte Enumeration der Zugfolgen zu ermitteln. Das resultierende erweiterte MIP-RNUM erfasst das Zusammenspiel von Infrastruktur, Eisenbahnbetrieb und Nachfrage und deren umfassende Auswirkungen auf die Netzwerkkapazität. Zuletzt wird das zeilengenerierende MIP-RNUM (MIP-RNUM-RG) vorgestellt, um auch die Kapazität großräumiger Instanzen untersuchen zu können. Der vorgestellte Ansatz begegnet der rechenzeitintensiven Enumeration der Elementarkreise des RNUM mit einer sog. lazy constraint generation, d. h. der iterativen, zeilengenerierenden Ergänzung verletzter Nebenbedingungen zum Problem. Um bei der Untersuchung großräumiger Instanzen die Lösungsqualität der jeweiligen Zwischenergebnisse beurteilen zu können, wird eine untere Schranke vorgestellt, die ein max-plus System höherer Ordnung mit einem binären Suchalgorithmus kombiniert. Diese untere Schranke ermöglicht die Zulässigkeitsprüfung einer gegebenen Lösung und darüber hinaus die Quantifizierung der Optimalitätslücke der aktuellen Ergebnisse. Damit stellt diese Arbeit verschiedene wissenschaftliche Beiträge in Form unterschiedlicher Untersuchungsmodelle und -methoden bereit, um die Kapazität komplexer Eisenbahnnetzwerke zu untersuchen. Dabei werden die verschiedenen infrastrukturellen, betrieblichen und nachfragespezifischen Perspektiven integriert betrachtet, um die nachfragezentrierte Netzentwicklung von Eisenbahnsystemen zu unterstützen. Unter Berücksichtigung des Wachstums der Eisenbahnnachfrage in naher Zukunft kann diese Arbeit so Planer*innen helfen, die Fähigkeiten unserer gegenwärtigen Eisenbahnsysteme zu untersuchen und daraus die nötigen Handlungsalternativen abzuleiten, um die Verkehrssysteme unserer Zukunft zu entwickeln.

The main part in the testing of the software is in the generation of test cases suitable for software system testing. The quality of the test cases plays a major role in reducing the time of software system testing and subsequently reduces the cost. The test cases, in model de- sign stages, are used to detect the faults before implementing it. This early detection offers more flexibility to correct the faults in early stages rather than latter ones. The best of these tests, that covers both static and dynamic software system model specifications, is one of the chal- lenges in the software testing. The static and dynamic specifications could be represented efficiently by Unified Modelling Language (UML) class diagram and sequence diagram. The work in this thesis shows that High Level Petri Nets (HLPN) can represent both of them in one model. Using a proper model in the representation of the software specifications is essential to generate proper test cases. The research presented in this thesis introduces novel and automated test cases generation techniques that can be used within a software sys- tem design testing. Furthermore, this research introduces e cient au- tomated technique to generate a formal software system model (HLPN) from semi-formal models (UML diagrams). The work in this thesis con- sists of four stages: (1) generating test cases from class diagram and Object Constraint Language (OCL) that can be used for testing the software system static specifications (the structure) (2) combining class diagram, sequence diagram and OCL to generate test cases able to cover both static and dynamic specifications (3) generating HLPN automat- ically from single or multi sequence diagrams (4) generating test cases from HLPN. The test cases that are generated in this work covered the structural and behavioural of the software system model. In first two phases of this work, the class diagram and sequence diagram are decomposed to nodes (edges) which are linked by Classes Hierarchy Table (CHu) and Edges Relationships Table (ERT) as well. The linking process based on the classes and edges relationships. The relationships of the software system components have been controlled by consistency checking technique, and the detection of these relationships has been automated. The test cases were generated based on these interrelationships. These test cases have been reduced to a minimum number and the best test case has been selected in every stage. The degree of similarity between test cases is used to ignore the similar test cases in order to avoid the redundancy. The transformation from UML sequence diagram (s) to HLPN facilitates the simpli cation of software system model and introduces formal model rather than semi-formal one. After decomposing the sequence diagram to Combined Fragments, the proposed technique converts each Combined Fragment to the corresponding block in HLPN. These blocks are con- nected together in Combined Fragments Net (CFN) to construct the the HLPN model. The experimentations with the proposed techniques show the effectiveness of these techniques in covering most of the software system specifications.