As camadas de enlace empregadas em redes sem fio de baixo custo e desempenho limitado, como as redes de sensores sem fio, são implementadas segundo o padrão IEEE 802.15.4. Prever o desempenho deste padrão é importante para analisar a viabilidade e o desempenho esperado de projetos envolvendo esse tipo de rede. Constatou-se que trabalhos anteriores com esse objetivo são incompletos no tocante às métricas aferidas e tem foco no cálculo de probabilidades, o que não faz parte da especificação do padrão. Assim, o objetivo deste trabalho foi projetar e implementar um modelo comportamental do padrão IEEE 802.15.4, cujos parâmetros possam ser facilmente alterados e que seja capaz de aferir as principais métricas de uma rede: vazão, taxa de entrega, atraso e gasto de energia. Os objetivos foram cumpridos com a validação do modelo perante simulação com o NS2. Além disso, o modelo foi utilizado para estudar a variação dos parâmetros aMaxFrameRetries, macMaxCSMABackos, initialCW e aUnitBackoPeriod do padrão IEEE 802.15.4, para estudar cenários em que os nós possuem tráfego assimétrico e cenários com diferentes relações de tamanho e taxa de chegada de pacotes, mantendo a taxa de bits constante. / Low cost and performance constrained wireless networks, such as wireless sensor networks, employ IEEE 802.15.4 standard as its MAC layer. Foreseeing this standard\'s performance is essential to analyze the feasibility and expected metrics results of these networks projects. It was observed that previous works with that aim are both incomplete regarding metrics of interest and focus on probability calculation, which is not part of the standard specication. Thus, the objective of this work is to project and implement a behavioral IEEE 802.15.4 standard model, which parameters may be easily set and that covers the main metrics of interest: throughput, delivery rate, delay and energy. The objectives were achieved, with model validation against NS2 simulations. Furthermore, the model was employed to analyze the performance variation caused by the parameters aMaxFrameRetries, macMaxCSMABackos, initialCW and aUnitBackoPeriod from the IEEE 802.15.4 standard and also scenarios with asymmetric trac conditions and packet size and arrival rate variations, maintaining a constant bitrate.

Ce travail s’inscrit dans le cadre d’étude de la sûreté de fonctionnement. La sûreté de fonctionnement est progressivement devenue partie intégrante de l’évaluation des performances des systèmes industriels. En effet, les pannes d’équipements, les pertes de production consécutives, et la maintenance des installations ont un impact économique majeur dans les entreprises. Il est donc essentiel pour un manager de pouvoir estimer de manière cohérente et réaliste les coûts de fonctionnement de l’entreprise, en tenant notamment compte des caractéristiques fiabilistes des équipements utilisés, ainsi que des coûts induits entre autres par le non-fonctionnement du système et la restauration des performances de ses composants après défaillance. Le travail que nous avons réalisé dans le cadre de ce doctorat se concentre sur un aspect particulier de la sûreté de fonctionnement, à savoir les politiques de remplacement d’équipements basées sur la fiabilité des systèmes qu’ils constituent. La recherche menée part de l’observation suivante : si la littérature consacrée aux politiques de remplacement est abondante, elle repose généralement sur l’hypothèse implicite que les nouveaux équipements envisagés présentent les mêmes caractéristiques et performances que celles que possédaient initialement les composants objets du remplacement. La réalité technologique est souvent bien différente de cette approche, quelle que soit la discipline industrielle envisagée. En effet, de nouveaux équipements sont régulièrement disponibles sur le marché ; ils assurent les mêmes fonctions que des composants plus anciens utilisés par une entreprise, mais présentent de meilleures performances, par exemple en termes de taux de défaillance, consommation d’énergie, " intelligence " (aptitude à transmettre des informations sur leur état de détérioration)... De plus, il peut devenir de plus en plus difficile de se procurer des composants de l’ancienne génération pour remplacer ceux qui ont été déclassés. Cette situation est généralement appelée obsolescence technologique. Le but de ce travail est de prolonger et d’approfondir, dans le cadre de la sûreté de fonctionnement, les réflexions engagées par les différents articles présentés dans la section état de l’art afin de définir et de modéliser des stratégies de remplacements d’équipements soumis à obsolescence technologique. Il s’agira de proposer un modèle, faisant le lien entre les approches plus économiques et celles plus fiabilistes, permettant de définir et d’évaluer l’efficacité, au sens large, des différentes stratégies de remplacement des unités obsolètes. L’efficacité d’une stratégie peut se mesurer par rapport à plusieurs critères parfois contradictoires. Parmi ceux-ci citons, évidemment, le coût total moyen engendré par la stratégie de remplacement, seul critère considéré dans les articles cités au chapitre 2, mais aussi la façon dont ces coûts sont répartis au cours du temps tout au long de la stratégie, la variabilité de ces coûts autour de leur moyenne, le fait de remplir certaines conditions comme par exemple d’avoir remplacé toutes les unités d’une génération par des unités d’une autre génération avant une date donnée ou de respecter certaines contraintes sur les temps de remplacement. Pour arriver à évaluer les différentes stratégies, la première étape sera de définir un modèle réaliste des performances des unités considérées, et en particulier de leur loi de probabilité de défaillance. Etant donné le lien direct entre la probabilité de défaillance d’un équipement et la politique de maintenance qui lui est appliquée, notamment la fréquence des maintenances préventives, leur effet, l’effet des réparations après défaillance ou les critères de remplacement de l’équipement, un modèle complet devra considérer la description mathématique des effets des interventions effectuées sur les équipements. On verra que la volonté de décrire correctement les effets des interventions nous a amené à proposer une extension des modèles d’âge effectif habituellement utilisés dans la littérature. Une fois le modèle interne des unités défini, nous développerons le modèle de remplacement des équipements obsolètes proprement dit. Nous appuyant sur la notion de stratégie K proposée dans de précédents travaux, nous verrons comment adapter cette stratégie K à un modèle pour lequel les temps d’intervention ne sont pas négligeables et le nombre d’équipes limité. Nous verrons aussi comment tenir compte dans le cadre de cette stratégie K d’une part des contraintes de gestion d’un budget demandant en général de répartir les coûts au cours du temps et d’autre part de la volonté de passer d’une génération d’unités à l’autre en un temps limité, ces deux conditions pouvant être contradictoires. Un autre problème auquel on est confronté quand on parle de l’obsolescence technologique est le modèle d’obsolescence à adopter. La manière dont on va gérer le risque d’obsolescence dépendra fortement de la manière dont on pense que les technologies vont évoluer et en particulier du rythme de cette évolution. Selon que l’on considère que le temps probable d’apparition d’une nouvelle génération est inférieur au temps de vie des composants ou supérieur à son temps de vie les solutions envisagées vont être différentes. Lors de deux applications numériques spécifiques. Nous verrons au chapitre 12 comment envisager le problème lorsque l’intervalle de temps entre les différentes générations successives est largement inférieur à la durée de vie des équipements et au chapitre 13 comment traiter le problème lorsque le délai entre deux générations est de l’ordre de grandeur de la durée de vie des équipements considérés. Le texte est structuré de la manière suivante : Après une première partie permettant de situer le contexte dans lequel s’inscrit ce travail, la deuxième partie décrit le modèle interne des unités tel que nous l’avons utilisé dans les différentes applications. La troisième partie reprend la description des stratégies de remplacement et des différentes applications traitées. La dernière partie permet de conclure par quelques commentaires sur les résultats obtenus et de discuter des perspectives de recherche dans le domaine.

La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple UPPAAL) et les réseaux de Petri temporisés (par exemple TINA). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec UPPAAL) et vers des réseaux de Petri temporisés (pour la vérification avec TINA). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.

This thesis considers the problem of performance modeling, analysis and control of capacitated re-entrant lines. Specifically, the first part of the thesis develops an analytical framework for the modeling, analysis and control of capacitated re-entrant lines, which is based on Generalized Stochastic Petri nets (GSPN) framework. The corresponding scheduling problem is systematically formulated, and the structure of the optimal policy is characterized and compared to that identified for "traditional" re-entrant lines. The second part of thesis addresses the problem of developing a systematic and computationally effective method for computing the optimal scheduling policy for any given configuration of capacitated re-entrant line. Specifically, the underlying scheduling problem is transformed to a Markov Decision Process (MDP) problem and an algorithm that systematically generates the MDP formulation for any given fab configuration is developed. The third part of thesis develops an effective approximating scheme based on the Neuro-Dynamic Programming (NDP) theory. In its general definition, the NDP method seeks the approximation of the optimal relative value function of the underlying MDP formulation by a parameterized function. Hence, an approximating structure for the considered problem is proposed and the quality of the generated approximations is systematically assessed. More specifically, this part of the thesis develops a set of "feature" functions and the mathematical apparatus necessary to evaluate the considered approximating scheme through a numerical experiment. The obtained results indicate that good quality approximations can be achieved by considering a set of features that characterize the distribution of the running process instances to the various processing stages and their lower order interactions. The last part of the thesis exploits the performance models developed in its earlier parts in order to provide an analytical characterization of the optimality of various deadlock resolution strategies for Markovian resource allocation systems under the objective of maximizing throughput.

Le contrôle de systèmes industriels à cause de l’automatisation et la réduction de nombre des opérateurs devient un enjeu crucial. Les systèmes de production automatisés (AMS) sont d’autant plus touchés car une défaillance du programme de contrôle peut réduire considérablement la productivité voire entraîner l’arrêt du système de production. Pour certains de ces systèmes où le partage des ressources est pondérant, la notion de blocage partiel ou global est fréquente et la validation avant implantation est préférable pour réduire les risques.En raison de la capacité des réseaux de Petri à décrire aisément l’exécution concurrente des processus et le partage des ressources, de nombreuses méthodes de vérification d’absence de blocage et de synthèse de contrôleurs basées sur la théorie structurelle ou le graphe d’accessibilité des réseaux de Petri ont été proposées au cours des deux dernières décennies.Traditionnellement, une méthode de prévention de blocage est évaluée selon trois critères de performance: la complexité structurelle, la permissivité comportementale, et la complexité de calcul. Les méthodes fondées sur l’espace d’état aboutissent généralement à un contrôle maximal permissif mais souffrent de l'explosion combinatoire de l'espace d'états. En revanche, les méthodes de synthèse de contrôleurs fondées sur l’analyse structurelle évitent le problème de l’explosion de l’espace d’état mais aboutissent à des superviseurs pouvant restreindre considérablement les comportements admissibles du système. De plus si la théorie structurelle de contrôle de siphons pour la synthèse des superviseurs est mature dans le cas des réseaux de Petri ordinaires, elle est en développement pour les réseaux de Petri généralises. Par ailleurs, la plupart des travaux existants partent du principe que les ressources sont constamment disponibles. Or l’indisponibilité de ressources est en réalité un phénomène ordinaire. Il serait donc judicieux de développer une politique de vérification de blocage qui soit efficace tout en considérant des ressources non fiables.Cette thèse vise principalement à faire face aux limitations mentionnées ci-dessus. Nos principales contributions à la fois théoriques et algorithmiques sont les suivantes.Premièrement, après avoir revisité les conditions de contrôlabilité des siphons (cs–propriété) et précisé les limitations de la max cs- propriété et max’ cs- propriété, nous définissons la max’’ cs-propriété et nous démontrons que cette nouvelle propriété est une condition non seulement suffisante mais aussi nécessaire pour la vivacité de la classe des GS3PR (Generalized Systems of SimpleSequential Processes with Resources).Par la suite nous montrons comment le problème de la vérification de cette propriété et donc la vivacité des GS3PR peut se ramener à la résolution d’un programme linéaire en nombre entiers.Dans une seconde partie, nous proposons une classe de réseaux de Petri appelée M-Nets dotée d’une forte capacité de modélisation des systèmes de production automatisés. En combinant la théorie du contrôle siphon avec la théorie des régions, nous développons une méthode de prévention de blocage ayant un bon compromis entre l'optimalité du comportement et la complexité de calcul. De plus, nous proposons une méthode de synthèse d'un contrôleur maximal permissif pour une sous-classe de réseaux notée b-nets.Enfin, nous proposons dans cette thèse une méthode de conception d’un superviseur de systèmes de production automatisés où les ressources ne sont pas toutes fiables et particulièrement efficace pour la classe des S3PR (Systems of Simple Sequential Processes with Resources). / Because of automation and reduction of the number of operators, the control of industrial systems is becoming a critical issue. For automated manufacturing systems (AMS) where resource sharing is preponderant, the notion of partial or total blocking is frequent and validation before implementation is preferable to reduce the risks.Due to the easy and concise description of the concurrent execution of processes and the resource sharing by Petri nets, many methods to verify deadlock-freeness and to synthesize controllers using structural theory or reachability graph have been proposed over the past two decades.Traditionally, a deadlock control policy can be evaluated by three performance criteria : structural complexity, behavioral permissiveness, and computational complexity. Generally, deadlock control policies based on the state space analysis can approach the maximal permissive behavior, but suffer from the state explosionproblem. On the contrary deadlock control policies based on the structural analysis of Petri nets avoid in general the state explosion problem successfully, but cannot lead to the maximally or near maximally permissive controller. Morover, the current Deadlock control theory based on siphons is fairly mature for ordinary Petri nets,while for generalized Petri nets, it is presently at an early stage.On the other hand, most deadlock control policies based on Petri nets for AMS proceed on the premise that the resources in a system under consideration are reliable. Actually, resource failures are inevitable and common in most AMS, which may also cause processes to halt. Therefore, it is judicious to develop an effective and robust deadlock control policy considering unreliable resources.This thesis aims to cope with the limitations mentioned above. Our main theoretical and algorithmic contributions are the following. Firstly, after revisiting the controllability conditions of siphons and limitations of max and max' controlled-siphon properties, we define the max'' cs property and we prove that this new cs-property is not only sufficient but also a necessary liveness condition forgeneralized systems of simple sequential processes with resources (GS3PR). Moreover, we show how the checking of this property and hence liveness of GS3PR nets can be translaled into resolution of an integer programming (IP) model.Secondly, we propose a class of manufacturing-oriented Petri nets, M-nets for short, with strong modeling capability. Combining siphon control and the theory of regions, we develop a deadlock prevention method that makes a good trade-off between behavioral optimality and computational tractability Moreover, this thesis proposes a maximally permissive control policy for a subclass of Petri nets (calledBéta-nets) based on the token distribution pattern of unmarked siphons.Finally, we propose a designs method for robust liveness-enforcingsupervisors for AMS with unreliable resources appropriate in particular for systems of simple sequential processes with resources(S3PR)

This thesis presents a framework to verify asynchronous real-time systems based on model checking. These systems are modeled by using a common modeling formalism named Labeled Petri-nets(LPNs). In order to verify the real-time systems algorithmically, the zone-based timing analysis method is used for LPNs. It searches the state space with timing information (represented by zones). When there is a high degree of concurrency in the model, firing concurrent enabled transitions in different order may result in different zones, and these zones may be combined without affecting the verification result. Since the zone-based method could not deal with this problem efficiently, the POSET timing analysis method is adopted for LPNs. It separates concurrency from causality and generates an exactly one zone for a single state. But it needs to maintain an extra POSET matrix for each state. In order to save time and memory, an improved zone-based timing analysis method is introduced by integrating above two methods. It searches the state space with zones but eliminates the use of the POSET matrix, which generates the same result as with the POSET method. To illustrate these methods, a circuit example is used throughout the thesis. Since the state space generated is usually very large, a graph data structure named multi-value decision diagrams (MDDs) is implemented to store the zones compactly. In order to share common clock value of dierent zones, two zone encoding methods are described: direct encoding and minimal constraint encoding. They ignore the unnecessary information in zones thus reduce the length of the integer tuples. The effectiveness of these two encoding methods is demonstrated by experimental result of the circuit example.

This thesis presents the computer implementation of a multi resolutional concurrent, design inference network, whose nodes are refined by PNDN (Petri Net Based Design Inference Network) modules. The extended design network is named as N-PNDN and consists of several embedded PNDN modules which models the information flow on a functional basis to facilitate the design automation at the conceptual design phase of an engineering design. Information flow in N-PNDN occurs between parent and child PNDN modules in a hierarchical structure and is provided by the token flow between the modules. In this study, computer implementation of the design network construction and token flow algorithms for the N-PNDN structure is restored and therefore the previous DNS (Design Network Simulator) is adapted for the multi layer design and decomposition of mechatronic products. The related algorithms are developed by using an object oriented, visual programming environment. The graphical user interface is also modified. The further developed DNS has been used for the application of the N-PNDN structure in the conceptual design of 5 mechatronic systems. In the guidance of this study, it has been understood that the further developed DNS is a powerful tool for designers coming from different engineering disciplines in order to interchange their ideas.

The factored state representation and concurrency semantics of Petri nets are closely related to those of classical planning models, yet automated planning and Petri net analysis have developed independently, with minimal and mainly unconvincing attempts at crossfertilisation. This thesis exploits the relationship between the formal reachability problem, and the automated planning problem, via Petri net unfolding, which is an attractive reachability analysis method for highly concurrent systems as it facilitates reasoning about independent sub-problems. The first contribution of this thesis is the theory of directed unfolding: controlling the unfolding process with informative strategies, for the purpose of optimality and increased efficiency. The second contribution is the application of directed unfolding to automated planning. Inspired by well-known planning heuristics, this thesis shows how problem specific information can be employed to guide unfolding, in response to the formal problem of developing efficient, directed reachability analysis methods for concurrent systems. Complimenting this theoretical work, this thesis presents a new forward search method for partial order planning which can be exponentially more efficient than state space search. Our suite of planners based on directed unfolding can perform optimal and suboptimal classical planning subject to arbitrary action costs, optimal temporal planning with respect to arbitrary action durations, and address probabilistic planning via replanning for the most likely path. Empirical results reveal directed unfolding is competitive with current state of the art automated planning systems, and can solve Petri net reachability problems beyond the reach of the original “blind” unfolding technique. / Thesis (Ph.D.) -- University of Adelaide, School of Electrical and Electronic Engineering, 2008

Cette thèse cherche à résoudre en pratique le problème de couverture dans les réseaux de Petri et les systèmes de canaux à pertes (LCS). Ces systèmes sont intéressants à étudier car ils permettent de modéliser facilement les systèmes concurrents et les systèmes distribués. Le problème de couverture dans un système de transitions consiste à savoir si on peut, à partir d’un état initial arriver à un état plus grand qu’un état cible. La résolution de ce problème dans les systèmes de transitions bien structurés (WSTS) sera le sujet d’études de la première partie. Les réseaux de Petri et les LCS sont des WSTS. On donnera dans la première partie une méthode générale pour le résoudre rapidement en pratique. Cette méthode utilise des invariants de couverture, qui sont des sur-approximations de l’ensemble des états couvrables. La seconde partie sera consacrée aux réseaux de Petri. Elle présentera diverses comparaisons théoriques et pratiques de différents invariants de couverture. Nous nous intéresserons notamment à la combinaison de l’invariant classique de l’inéquation d’état avec une analyse de signe simple. Les LCS seront le sujet d’études de la troisième partie. On présentera une variante de l’inéquation d’état adaptée aux LCS ainsi que deux invariants qui retiennent des propriétés sur l’ordre dans lequel les messages sont envoyés. La thèse a mené à la création de deux outils, ICover et BML, pour résoudre le problème de couverture respectivement dans les réseaux de Petri et dans les LCS. / The goal of this thesis is to solve in practice the coverability problem in Petri nets and lossy channel systems (LCS). These systems are interesting to study because they can be used to model concurrent and distributed systems. The coverability problem in a transition system is to decide whether it is possible, from an initial state, to reach a greater state than a target state. In the first part, we discuss how to solve this problem for well-structured transition systems (WSTS). Petri nets and LCS are WSTS. In the first part, we present a general method to solve this problem quickly in practice. This method uses coverability invariants, which are over-approximations of the set of coverable states. The second part studies Petri nets.We present comparisons of coverability invariants, both in theory and in practice. A particular attention will be paid on the combination of the classical state inequation and a simple sign analysis. LCS are the focus of the third part. We present a variant of the state inequation for LCS and two invariants that compute properties for the order in which messages are sent. Two tools, ICover and BML, were developed to solve the coverability problem in Petri nets and LCS respectively.

Trabalhos recentes na área de Planejamento e Escalonamento têm gerado uma grande expectativa em relação à aplicação dos resultados em sistemas reais. Neste cenário, métodos, ferramentas e conceitos provenientes das Engenharia do Conhecimento e da Engenharia de Requisitos se tornam fundamentais para caracterizar melhor, entender e especificar os domínios de planejamento. Nesse caso uma especial importância deve ser dada às etapas iniciais do processo, onde o conhecimento sobre o domínio é incompleto e onde existem poucas ferramentas, seja para o suporte ou automação parcial do processo, e as ferramentas já existentes carecem de métodos formais para a modelagem e análise dos requisitos. Neste trabalho propõe-se o ReKPlan (Ambiente para a Engenharia de Requisitos usando KAOS em problemas de planejamento), que usa KAOS, um método orientado a objetivos, para a modelagem de requisitos. Entretanto, o uso do KAOS (ou de qualquer outro método goaloriented) não atende à necessidade de verificar formalmente o comportamento dinâmico quando o alvo são sistemas de planejamento. A proposta deste trabalho é combinar o uso do método orientado a objetivos com o formalismo das Redes de Petri (Rdp) -especificamente a abordagem seguida pelo GHENeSys- para representar e analisar requisitos no projeto de sistemas de planejamento. Finalmente é proposto um método sobre o processo de projeto que, guiado por modelos, gera instruções PDDL servindo de entrada para os planejadores. A método foi aplicado a vários estudos de caso que o avaliam como um mecanismo promissor e eficiente na Engenharia de Requisitos resultando em uma melhor definição dos requisitos em problemas de planejamento. / Recent works in Planning and Scheduling, lead to a great expectations about how to apply achieved results in real systems. In this scenario, methods, tools and concepts from Knowledge and Requirements Engineering seem to be a key issue for characterizing, understanding and specifying the domain of planning problems. In this case a special attention should be given to the initial stages of the process, where knowledge about the domain is incomplete and there are a few tools to support or partially automate the process, and there is a lack of formal methods for modeling and analysis of requirements in the existing tools. This work proposes the ReKPlan (Requirement Engineering Using KAOS for Planning Problems) which uses KAOS, a goal-oriented method, for modeling requirements. However, the use of KAOS (or another goal-oriented method) don\'t seem the most appropriate for formal verification of the dynamic behavior of planning systems. The purpose of this work is to combine the use of KAOS with Petri Nets formalism (Rdp) - GHENeSys approach specifically - for modeling and analyzing requirements in the design of planning system. Finally is proposed a model driven engineering mechanism over a design for guiding, until the generation of PDDL instructions as input for planners to solve problems.