L'objet des travaux de cette thèse est de proposer de nouveaux processus de définition de tests (testabilité), de nouvelles méthodes de tests, ainsi que de nouvelles méthodes d'interprétation des tests (diagnostic). Ces travaux ont été menés dans le cadre de l'aéronautique et ont porté dans un premier temps sur l'identification des besoins en diagnostic des hélicoptères. Les problématiques liées au test et au diagnostic des hélicoptères portaient sur : - La non-détection de certaines défaillances - L'occurrence de nombreuses fausses alarmes - L'ambiguïté de localisation de défaillances Dans un premier temps nous avons réalisé l'état de l'art des recherches en diagnostic, ceci afin de sélectionner les technologies et méthodologies permettant de répondre aux problématiques identifiées. Les technologies candidates ont ensuite été architecturées afin de proposer un traitement intégré permettant de répondre à l'ensemble des besoins identifiés. Ainsi nous avons travaillé sur les méthodologies de définition du test, aux moyens d'outils de simulation de la testabilité. Nous avons aussi défini de nouvelles méthodes de test permettant de déterminer l'état de capteurs analogiques aux moyens d'algorithmes basés sur des évaluateurs de calcul de variation de l'écart type, du facteur de forme et du rapport signal sur bruit. Nous avons ensuite travaillé sur l'amélioration du diagnostic au niveau système à l'aide d'automates temporisés afin de simuler le fonctionnement des arbres de tests élémentaires. Ces travaux ont ensuite conduit à la modélisation et au diagnostic des systèmes complexes à l'aide des diagrammes d'état, des arbres de défaillances dynamiques, ainsi que leur simulation à l'aide des réseaux de Petri. Les modèles utilisés ont été complétés au moyen de nouvelles portes dynamiques. Ces travaux ont été appliqués au monde aéronautique, sur plusieurs hélicoptères et ont fait l'objet de deux brevets.

Les travaux de thèse concernent la mise en oeuvre d'une maintenance distribuée dans les systèmes manufacturiers. Notre problématique s'est portée sur la mise en place d'un service de maintenance destiné à un réseau d'entreprises de plusieurs sites de production. Ces sites sont répartis géographiquement avec des distances importantes intersites, et dont la réparation des parties défaillantes requiert des ressources particulières situées dans un atelier central. Il s'agit donc de la mise en oeuvre d'une démarche de conception d'ateliers de maintenance et dimensionnement des ressources dans un contexte distribué. On se place dans le cas où l'on dispose : 1. d'un atelier de maintenance central qui prend en charge les réparations des équipements défaillants, c'est l'AdM Central ; 2. d'un atelier de maintenance mobile qui effectue des actions de maintenance préventives sur plusieurs sites répartis géographiquement, c'est l'AdM mobile ; 3. un ensemble de sites de production ; Pour un budget donné, l'objectif est de proposer une démarche méthodologique permettant de dimensionner les ressources communes (pièces de rechange et opérateurs de maintenance), de proposer une politique d'inspection adéquate de l'atelier mobile et d'ordonnancer les tâches de maintenance. Nous proposons, dans ce contexte de maintenance distribuée, une méthodologie permettant de minimiser la fonction coût. À partir d'une structure multi-sites, une démarche de modélisation modulaire et d'analyse est proposée. Le réseau d'ateliers de maintenance est modélisé par une forme de Réseaux de Petri Stochastiques Synchronisés (RdPSSy). Passant par le calcul du parcours optimal, l'étape d'évaluation des coûts est effectuée par simulation des modèles développés en utilisant la toolbox Stateflow de Matlab. cas de panne aléatoire sur un site de production est pris en compte.

Les travaux résumés dans ce mémoire ont pour cadre la sûreté de fonctionnement des systèmes informatiques. Ils couvrent plusieurs aspects complémentaires, à la fois théoriques et expérimentaux, que nous avons groupés en quatre thèmes. Le premier thème traite de la définition de méthodes permettant de faciliter la construction et la validation de modèles complexes pour l'analyse et l'évaluation de la sûreté de fonctionnement. Deux approches sont considérées : les réseaux de Petri stochastiques généralisés et la simulation comportementale en présence de fautes. Le deuxième thème traite de la modélisation de la croissance de fiabilité pour évaluer l'évolution de la fiabilité et de la disponibilité des systèmes en tenant compte de l'élimination progressive des fautes de conception. Ces travaux sont complétés par la définition d'une méthode permettant de faciliter la mise en ¿uvre d'une étude de fiabilité de logiciel dans un contexte industriel. Le troisième thème concerne la définition et l'expérimentation d'une approche pour l'évaluation quantitative de la sécurité-confidentialité. Cette approche permet aux administrateurs des systèmes de suivre l'évolution de la sécurité opérationnelle quand des modifications, susceptibles d'introduire de nouvelles vulnérabilités, surviennent dans la configuration opérationnelle, les applications, le comportement des utilisateurs, etc. Enfin, le quatrième thème porte d'une part, sur l'élaboration d'un modèle de développement destiné à la production de systèmes sûrs de fonctionnement, et d'autre part, sur la définition de critères d'évaluation visant à obtenir une confiance justifiée dans l'aptitude des systèmes à satisfaire leurs exigences de sûreté de fonctionnement, en opération et jusqu'au retrait du service.

Ce mémoire présente des travaux et des résultats, aussi bien théoriques que pratiques, concernant la<br />modélisation et l'évaluation de la croissance de fiabilité et de la croissance de disponibilité des<br />systèmes informatiques. Nous considérons deux types de représentation du comportement des<br />systèmes : d'abord, en fonction du temps, et ensuite en fonction du nombre d'exécutions effectuées.<br />Les travaux présentés dans ce mémoire s'articulent autour de deux modèles de croissance de fiabilité : le<br />modèle hyperexponentiel en temps continu et le modèle hyperexponentiel en temps discret. Pour<br />chacun de ces deux modèles, nous étudions d'abord, le cas d'un système mono-composant, puis nous<br />considérons le cas d'un système multi-composant qui est tel que la croissance de fiabilité de chacun de<br />ses composants est représentée par un modèle hyperexponentiel. Le modèle hyperexponentiel en<br />temps discret est également utilisé pour prendre en compte certaines caractéristiques de<br />l'environnement d'utilisation du logiciel dans l'évaluation de son comportement tel qu'il est perçu<br />dans le temps par ses utilisateurs dans chacun des environnements dans lequel il est mis en oeuvre.

Comprendre la genèse d’une situation de conduite requiert d’analyser les choixfaits par le conducteur au volant de son véhicule pendant l’activité de conduite, dans sacomplexité naturelle et dans sa dynamique située. Le LESCOT a développé le modèleCOSMODRIVE, fournissant un cadre conceptuel pour la simulation cognitive de l’activitéde conduite automobile. Pour exploiter ce modèle en simulation, il est nécessairede produire les connaissances liées à la situation de conduite sous forme d’un automatepar exemple. La conception d’un tel automate nécessite d’une part de disposer de donnéesissues de la conduite réelle, enregistrées sur un véhicule instrumenté et d’autrepart d’une expertise humaine pour les interpréter.Pour accompagner ce processus d’ingénierie des connaissances issues de l’analysed’activité, ce travail de thèse propose une méthode de découverte interactive deconnaissances à partir de traces d’activité. Les données de conduite automobile sontconsidérées comme des M-Traces, associant une sémantique explicite aux données,exploitées en tant que connaissances dans un Système à Base de Traces (SBT). Le SBTpermet de filtrer, transformer, reformuler et abstraire les séquences qui serviront à alimenterla synthèse de modèles automates de l’activité de conduite. Nous reprenons destechniques de fouille de workflow permettant de construire des automates (réseaux dePetri) à partir de logs. Ces techniques nécessitent des données complètes ou statistiquementreprésentatives. Or les données collectées à bord d’un véhicule en situationde conduite sont par nature des cas uniques, puisqu’aucune situation ne sera jamaisreproductible à l’identique, certaines situations particulièrement intéressantes pouvanten outre être très rarement observées. La gageure est alors de procéder à une forme degénéralisation sous la forme de modèle, à partir d’un nombre de cas limités, mais jugéspertinents, représentatifs, ou particulièrement révélateurs par des experts du domaine.Pour compléter la modélisation de telles situations, nous proposons donc de rendreinteractifs les algorithmes de synthèse de réseau de Petri à partir de traces, afin depermettre à des experts-analystes de guider ces algorithmes et de favoriser ainsi la découvertede connaissances pertinentes pour leur domaine d’expertise. Nous montreronscomment rendre interactifs l’algorithme α et l’algorithme α+ et comment généralisercette approche à d’autres algorithmes.Nous montrons comment l’utilisation d’un SBT et de la découverte interactived’automates impacte le cycle général de découverte de connaissances. Une méthodologieest proposée pour construire des modèles automates de l’activité de conduiteautomobile.Une étude de cas illustre la méthodologie en partant de données réelles de conduiteet en allant jusqu’à la construction de modèles avec un prototype logiciel développédans le cadre de cette thèse / Driving is a dynamic and complex activity. Understanding the origin of a driving situationrequires the analysis of the driver’s choices made while he/she drives. In addition,a driving situation has to be studied in its natural complexity and evolution. LESCOThas developed a model called COSMODRIVE, which provides a conceptual frameworkfor the cognitive simulation of the activity of car driving. In order to run themodel for a simulation, it is necessary to gather knowledge related to the driving situation,for example in the form of an automaton. The conception of such an automatonrequires : 1) the use of real data recorded in an instrumented car, and, 2) the use of humanexpertise to interpret these data. These data are considered in this thesis as activitytraces.The purpose of this thesis is to assist the Knowledge Engineering process of activityanalysis. The present thesis proposes a method to interactively discover knowledgefrom activity traces. For this purpose, data from car driving are considered as M-traces– which associate an explicit semantic to these data. This semantic is then used asknowledge in a Trace Based System. In a Trace Based System, M-traces can be filtered,transformed, reformulated, and abstracted. The resulting traces are then used as inputsin the production of an automaton model of the activity of driving. In this thesis,Workflow Mining techniques have been used to build automata (Petri nets) from logs.These techniques require complete or statistically representative data sets. However,data collected from instrumented vehicles are intrinsically unique, as no two drivingsituations will ever be identical. In addition, situations of particular interest, such ascritical situations, are rarely observed in instrumented vehicle studies. The challenge isthen to produce a model which is a form of generalisation from a limited set of cases,which have been judged by domain experts as being relevant and representative of whatactually happens.In the current thesis, algorithms synthesising Petri nets from traces have been madeinteractive, in order to achieve the modelling of such driving situations. This thenmakes it possible for experts to guide the algorithms and therefore to support the discoveryof knowledge relevant to the experts. The process involved in making the α-algorithm and the α+-algorithm interactive is discussed in the thesis in a way that canbe generalised to other algorithms.In addition, the current thesis illustrates how the use of a Trace Based System andthe interactive discovery of automata impacts the global cycle of Knowledge Discovery.A methodology is also proposed to build automaton models of the activity of cardriving. Finally, a case study is presented to illustrate how the proposed methodologycan be applied to real driving data in order to construct models with the softwaredeveloped in this thesis

La complexification des systèmes et la réduction du nombre de capteurs nécessitent l’élaboration de méthodes de surveillance de plus en plus efficaces. Le travail de cette thèse s’inscrit dans ce contexte et porte sur le diagnostic et le pronostic des Systèmes à Événements Discrets (SED) temporisés. Les réseaux de Petri stochastiques partiellement mesurés sont utilisés pour modéliser le système. Le modèle représente à la fois le comportement nominal et le comportement dysfonctionnel du système. Il permet aussi de représenter ses capteurs à travers une mesure partielle des transitions et des places. Notre contribution porte sur l’exploitation de l’information temporelle pour le diagnostic et le pronostic des SED. À partir d’une suite de mesures datées, les comportements du système qui expliqueraient ces mesures sont d’abord déterminés. La probabilité de ces comportements est ensuite évaluée pour fournir un diagnostic du système en termes de probabilité d’occurrence d’un défaut. Dans le cas où une faute est diagnostiquée, une approche permettant d’estimer la distribution de sa date d’occurrence est proposée. L’objectif est de donner plus de détails sur cette faute afin de mieux la caractériser. Par ailleurs, la probabilité des comportements compatibles est exploitée pour estimer l’état actuel du système. Il s’agit de déterminer les marquages compatibles avec les mesures ainsi que leurs probabilités associées. À partir de cette estimation d’état, la prise en considération des évolutions possibles du système permet d’envisager la prédiction de la faute avant son occurrence. Une estimation de la probabilité d’occurrence de la faute sur un horizon de temps futur est ainsi obtenue. Celle-ci est ensuite étendue à l’évaluation de la durée de vie résiduelle du système. Enfin, une application des différentes approches développées sur un cas d’un système de tri est proposée. / Due to the increasing complexity of systems and to the limitation of sensors number, developing monitoring methods is a main issue. This PhD thesis deals with the fault diagnosis and prognosis of timed Discrete Event Systems (DES). For that purpose, partially observed stochastic Petri nets are used to model the system. The model represents both the nominal and faulty behaviors of the system and characterizes the uncertainty on the occurrence of events as random variables with exponential distributions. It also considers partial measurements of both markings and events to represent the sensors of the system. Our main contribution is to exploit the timed information, namely the dates of the measurements for the fault diagnosis and prognosis of DES. From the proposed model and collected measurements, the behaviors of the system that are consistent with those measurements are obtained. Based on the event dates, our approach consists in evaluating the probabilities of the consistent behaviors. The probability of faults occurrences is obtained as a consequence. When a fault is detected, a method to estimate its occurrence date is proposed. From the probability of the consistent trajectories, a state estimation is deduced. The future possible behaviors of the system, from the current state, are considered in order to achieve fault prediction. This prognosis result is extended to estimate the remaining useful life as a time interval. Finally, a case study representing a sorting system is proposed to show the applicability of the developed methods.

L'usage excessif des routes peut entraîner de nombreux inconvénients dont la pollution, les accidents et la congestion. Une solution accessible à court terme consiste à mettre en œuvre des systèmes de gestion de trafic. Dans ce cadre, nous proposons un formalisme, appelé Réseaux de Petri Lots Triangulaire, qui permet la modélisation et la simulation du trafic routier au niveau mésoscopique comme un système à événements discrets. Le RdPLots Triangulaire permet ainsi de décrire les caractéristiques globales du trafic routier: flux, densité et vitesse à travers la proposition d'une relation flux-densité triangulaire. Cette relation implique une modification de la dynamique des lots. Cette dynamique permet maintenant de représenter les deux états du trafic routier à savoir fluide et congestionné ainsi que les trois régimes dédiés au comportement libre, congestion et décongestion. Le calcul des flux instantanés des transitions est à présent réalisé par une méthode basée sur la technique de programmation linéaire en ajoutant une contrainte qui prend en compte l'état et le régime des lots. Pour modéliser des stratégies de contrôle telles que la variation de la vitesse limite (VSL), nous avons intégré au RdPLots Triangulaire des événements contrôlés qui permettent le changement de la vitesse maximale d'une place lot et le flux maximal d'une transition continue ou lot. Tous ces apports théoriques sont implémentés dans un logiciel que nous avons appelé SimuleauTri, sous lequel nous avons étudié des portions d'autoroute à partir des données réelles. Les résultats de simulation sont proches des mesures effectuées sur le terrain, et montrent la pertinence de RdPLots Triangulaire. / The excessive use of roads can cause many adverse effects including pollution, insecurity and congestion. The available short-term solution is the implementation of traffic management systems which optimize the flow and reduce congestion without needing additional infrastructures. In this context, we proposed a new formalism, called Triangular Batches Petri Nets (Triangular BPN), which combines modeling and simulation of traffic in mesoscopic level as a discrete event system. The Triangular BPN describing the overall characteristics of the road traffic such as flow, density, speed by representing a new triangular relation flow-density. This relation implies the modification of batches dynamic, which is now used to represent the two road traffic states : fluid and congested, as well as the three behaviors :free, congestion and decongestion. The calculation of the instantaneous firing flows is achieved by adding a constraint that takes into account the state and behavior of batches. A set of controlled events integrated to the Triangular BPN, that allow the variation of the maximum speed of batch place and the maximum flow of batch and continuous transition. These controlled events used to model the control strategies, such as variable speed limit (VSL). All these theoretical contributions implemented in a software that is called SimuleauTri and used to study a motorway portions from real data. The simulation results are close to the measurements on the ground and show the pertinence of Triangular BPN.

Le travail présenté dans cette thèse a lieu dans le domaine de développement basé sur les composants, il est une contribution à laspécification, l'adaptation et la vérification des systèmes à base de composants. Le but principal de cette thèse est la proposition d'uneapproche formelle pour construire progressivement des systèmes complexes en assemblant et en adaptant un ensemble de composants,où leur structure et leur comportement sont modélisés à l'aide de diagrammes SysML. Dans la première étape, nous avons défini uneapproche basée sur la méta-modélisation et la transformation des modèles pour vérifier la compatibilité des blocs ayant leurs protocolesd'interaction modélisés à l'aide de diagrammes de séquence SysML. Pour vérifier leur compatibilité, nous effectuons une transformationen automates d'interface (IAs), et nous utilisons l'approche optimiste définie sur les IA. Cette approche considère que deux composantssont compatibles s'il existe un environnement approprié avec lequel ils peuvent interagir correctement. Après cela, nous avons proposéde bénéficier de la hiérarchie, qui peut être présente dans les modèles de protocole d'interaction des blocs, pour alléger la vérification dela compatibilité des blocs. Dans l'étape suivante, nous avons pris en considération le problème des incohérences de noms de type one2oneentre les services des blocs. A ce stade, un adaptateur est généré pour un ensemble de blocs réutilisés qui ont leurs protocoles d'interactionmodélisés formellement par des automates d'interface. La génération de l'adaptateur est guidée par la spécification du bloc parent qui estfaite initialement par le concepteur. Notre approche est complétée par une phase de vérification qui nous permet de vérifier les exigencesSysML, exprimées formellement par les propriétés temporelles, sur les blocs SySML. Dans cette phase, nous avons exploité uniquementles adaptateurs générés pour vérifier la préservation des exigences initialement satisfaites par les blocs réutilisés. Ainsi, notre approchea l'intention de donner plus de chance d'éviter le problème de l'explosion de l'espace d'état au moment de la vérification. Dans le mêmecontexte, où nous avons un ensemble de blocs réutilisés et la spécification de leurs blocs parents, nous avons proposé d'utiliser des réseauxde Petri colorés (CPN) pour modéliser les interactions des blocs et générer des adaptateurs qui résolvent plus de types de problèmes. Dansce cas, l'adaptateur peut résoudre le problème de blocage en permettant le ré-ordonnancement des appels de services. / The work presented in this thesis takes place in the component-based development domain, it is a contribution to the specification,adaptation and verification of component-based systems. The main purpose of this thesis is the proposition of a formal approach tobuild incrementally complex systems by assembling and adapting a set of components, where their structure and behaviour are modelledusing SysML diagrams. In the first stage, we have defined a meta-model driven approach which is based on meta-modelling and modelstransformation, to verify the compatibility of blocks having their interaction protocols modelled using SysML sequence diagrams. To verifytheir compatibility, we perform a transformation into interface automata (IAs), and we base on the optimistic approach defined on IAs. Thisapproach consider that two components are compatible if there is a suitable environment with which they can interact correctly. Afterthat, we have proposed to benefit from the hierarchy, that may be present in the interaction protocol models of the blocks, to alleviate theverification of blocks compatibility. In the next stage, we have taken into consideration the problem of names mismatches of type one2onebetween services of blocks. At this stage, an adapter is generated for a set of reused blocks which have their interaction protocols modelledformally by interface automata. The generation of the adapter is guided by the specification of the parent block which is made initiallyby the designer. Our approach is completed by a verification phase which allows us to verify SysML requirements, expressed formallyby temporal properties, on SySML blocks. In this phase, we have exploited only the generated adapters to verify the preservation of therequirements initially satisfied by the reused blocks. Thus, our approach intends to give more chance to avoid the state space explosionproblem during the verification. In the same context, where we have a set of reused blocks and the specification of their parent blocks, wehave proposed to use coloured Petri nets (CPNs) to model the blocks interactions and to generate adapters that solve more type of problems.In this case the adapter can solve the problem of livelock by enabling the reordering of services calls.

Les Réseaux de Petri (RdP) sont actuellement les approches les plus prometteuses pour modéliser et vérifier les systèmes complexes tels que les Systèmes Multi Agents (SMA). De nombreuses solutions ont été proposées pour remédier aux problèmes de communication, de coordination et d’interaction entre les Agents. Cependant, il n’existe aucune en mesure de traiter, à la fois les aspects structurels et comportementaux, du moins à notre connaissance. La thèse s'intéresse à la problématique de modélisation formelle et de vérification automatique et semi-automatique de propriétés pour les Systèmes Multi Agents. Plus précisément, l'objectif consiste à proposer un nouveau modèle formel original basé sur les réseaux de Petri, les Réseaux de Petri à Agents (RdPA), qui permettent d’exprimer de manière consistante et plus précise les systèmes Multi Agents. Il s’intéresse de plus à l’extension de ce modèle aux fins de modéliser la migration des agents dans le cadre des systèmes à agents mobiles. Cette classe de modèle permet de s’intéresser à la vérification formelle de propriétés classiques comme notamment la vivacité ou l’absence d’interblocage dans le cadre des Systèmes Multi-Agent. / Petri nets (PN) are currently the most promising approaches to model and to verify complex systems such as Multi Agent Systems (MAS). Several solutions have been proposed to solve the problems of communication, coordination and interaction among Agents. However, to best of our knowledge, none of this solution has able to handle both aspects: structural and behavioral. The thesis focuses on the problem of formal modeling and automatic and semi-automatic verification of properties in Multi Agent Systems. More specifically, the objective is to propose a new original formal model based on Petri nets, Agents Petri nets (APN), which express consistently more accurate a Multi Agent Systems. There is growing interest in the extension of this model for modeling the migration of Agents within the mobile Agent systems. This class of model allows focusing on the formal verification of classical properties such as alertness or absence of deadlock in the context of Multi Agent Systems.

Réalisé en cotutelle avec l'École normale supérieure de Cachan – Université Paris-Saclay / L'un des aspects fondamentaux des systèmes informatiques modernes, et en particulier des systèmes critiques, est la possibilité d'exécuter plusieurs processus, partageant des ressources communes, de façon simultanée. De par leur nature concurrentielle, le bon fonctionnement de ces systèmes n'est assuré que lorsque leurs comportements ne dépendent pas d'un ordre d'exécution prédéterminé. En raison de cette caractéristique, il est particulièrement difficile de s'assurer qu'un système concurrent ne possède pas de faille. Dans cette thèse, nous étudions la vérification formelle, une approche algorithmique qui vise à automatiser la vérification du bon fonctionnement de systèmes concurrents en procédant par une abstraction vers des modèles mathématiques. Nous considérons deux de ces modèles, les réseaux de Petri et les systèmes d'addition de vecteurs, et les problèmes de vérification qui leur sont associés. Nous montrons que le problème d'accessibilité pour les systèmes d'addition de vecteurs (avec états) à deux compteurs est PSPACE-complet, c'est-à-dire complet pour la classe des problèmes solubles à l'aide d'une quantité polynomiale de mémoire. Nous établissons ainsi la complexité calculatoire précise de ce problème, répondant à une question demeurée ouverte depuis plus de trente ans. Nous proposons une nouvelle approche au problème de couverture pour les réseaux de Petri, basée sur un algorithme arrière guidé par une caractérisation logique de l'accessibilité dans les réseaux de Petri continus. Cette approche nous a permis de mettre au point un nouvel algorithme qui s'avère particulièrement efficace en pratique, tel que démontré par notre implémentation logicielle nommée QCover. Nous complétons ces résultats par une étude des systèmes de transitions bien structurés qui constituent une abstraction générale des systèmes d'addition de vecteurs et des réseaux de Petri. Nous considérons le cas des systèmes de transitions bien structurés à branchement infini, une classe qui inclut les réseaux de Petri possédant des arcs pouvant consommer ou produire un nombre arbitraire de jetons. Nous développons des outils mathématiques facilitant l'étude de ces systèmes et nous délimitons les frontières au-delà desquelles la décidabilité des problèmes de terminaison, de finitude, de maintenabilité et de couverture est perdue. / One fundamental aspect of computer systems, and in particular of critical systems, is the ability to run simultaneously many processes sharing resources. Such concurrent systems only work correctly when their behaviours are independent of any execution ordering. For this reason, it is particularly difficult to ensure the correctness of concurrent systems. In this thesis, we study formal verification, an algorithmic approach to the verification of concurrent systems based on mathematical modeling. We consider two of the most prominent models, Petri nets and vector addition systems, and their usual verification problems considered in the literature. We show that the reachability problem for vector addition systems (with states) restricted to two counters is PSPACE-complete, that is, it is complete for the class of problems solvable with a polynomial amount of memory. Hence, we establish the precise computational complexity of this problem, left open for more than thirty years. We develop a new approach to the coverability problem for Petri nets which is primarily based on applying forward coverability in continuous Petri nets as a pruning criterion inside a backward coverability framework. We demonstrate the effectiveness of our approach by implementing it in a tool named QCover. We complement these results with a study of well-structured transition systems which form a general abstraction of vector addition systems and Petri nets. We consider infinitely branching well-structured transition systems, a class that includes Petri nets with special transitions that may consume or produce arbitrarily many tokens. We develop mathematical tools in order to study these systems and we delineate the decidability frontier for the termination, boundedness, maintainability and coverability problems.