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.

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.

L'identification des interactions survenant au niveau moléculaire joue un rôle crucial pour la compréhension du vivant. L'objectif de ce travail a consisté à développer des méthodes permettant de modéliser et de prédire ces interactions pour le métabolisme et la régulation de la transcription. Nous nous sommes basés pour cela sur la modélisation de ces systèmes sous la forme de graphes et d'automates. Nous avons dans un premier temps développé une méthode permettant de tester et de prédire la distribution du flux au sein d'un réseau métabolique en permettant la formulation d'une à plusieurs contraintes. Nous montrons que la prise en compte des données biologiques par cette méthode permet de mieux reproduire certains phénotypes observés in vivo pour notre modèle d'étude du métabolisme énergétique du parasite Trypanosoma brucei. Les résultats obtenus ont ainsi permis de fournir des éléments d'explication pour comprendre la flexibilité du flux de ce métabolisme, qui étaient cohérentes avec les données expérimentales. Dans un second temps, nous nous sommes intéressés à une catégorie particulière d'ARN non codants appelés sRNAs, qui sont impliqués dans la régulation de la réponse cellulaire aux variations environnementales. Nous avons développé une approche permettant de mieux prédire les interactions qu'ils effectuent avec d'autres ARN en nous basant sur une prédiction des interactions, une analyse par enrichissement du contexte biologique de ces cibles, et en développant un système de visualisation spécialement adapté à la manipulation de ces données. Nous avons appliqué notre méthode pour l'étude des sRNAs de la bactérie Escherichia coli. Les prédictions réalisées sont apparues être en accord avec les données expérimentales disponibles, et ont permis de proposer plusieurs nouvelles cibles candidates. / The identification of the interactions occurring at the molecular level is crucial to understand the life process. The aim of this work was to develop methods to model and to predict these interactions for the metabolism and the regulation of transcription. We modeled these systems by graphs and automata.Firstly, we developed a method to test and to predict the flux distribution in a metabolic network, which consider the formulation of several constraints. We showed that this method can better mimic the in vivo phenotype of the energy metabolism of the parasite Trypanosoma brucei. The results enabled to provide a good explanation of the metabolic flux flexibility, which were consistent with the experimental data. Secondly, we have considered a particular class of non-coding RNAs called sRNAs, which are involved in the regulation of the cellular response to environmental changes. We developed an approach to better predict their interactions with other RNAs based on the interaction prediction, an enrichment analysis, and by developing a visualization system adapted to the manipulation of these data. We applied our method to the study of the sRNAs interactions within the bacteria Escherichia coli. The predictions were in agreement with the available experimental data, and helped to propose several new target candidates.