Presently, most spacecraft are controlled from ground involving activities such as up-linking the schedule of daily operations and monitoring health parameters. These activities lead to a cognitive overload on human operators. Imaging/science opportunities are lost, if any discrepancies occur during the execution of pre-planned sequences. Consequently, advanced space exploration systems for future needs demand on-board intelligence and autonomy. This thesis attempts to solve the problem of providing an adequate degree of autonomy in future generation of spacecraft. The autonomous spacecraft accept high-level goals from users and make decisions on-board to generate detailed command schedules satisfying stringent constraints posed by the harsh environment of the space, visibility criteria and scarce on-board resources. They reconfigure themselves in case of any failure and re-plan when needed. Autonomy concepts are derived in the context of complex systems by drawing analogy to living organisms and social organisations. A general autonomy framework may be defined with a six level structure comprising of the following capabilities -reflexes, awareness, self-regulation, self-healing, self-adaptation and self-evolution. A generic and reusable software architecture is proposed using hybrid multi-agent systems, which are arranged in a hierarchical manner using two types of decomposition viz. stratum and layer. The software architecture of the autonomous spacecraft is modeled as a stratified agent with a deliberative stratum, which achieves adaptive behaviour and a reactive stratum, which achieves reactive behaviour. Each individual agent has a generic structure comprising of perception, action, communication and knowledge components. It achieves the specialist capability through model-based reasoning. The knowledge models encompass: Planning knowledge describing higher-level goals, task structure and method of achieving the goals, Control knowledge encompassing the static and dynamic models of the spacecraft and Diagnostic knowledge incorporating the cause-effect relationships. The deliberative stratum is capable of planning in different time horizons and is, in turn, organised into a hierarchical agent system with three layers corresponding to different time horizons. It is composed of a long-term, medium-term and short-term planning agents, focusing on strategic issues, spacecraft level resources and specific spacecraft states respectively. The power of Petri nets is exploited for knowledge modeling as well as for plan representation. The ability of Petri nets to represent causality, concurrency and conflict relations explicitly makes it an excellent tool for representing the planning problem. Hierarchical Timed Petri Net is chosen for our modeling, since it captures the temporal requirements of the real-time spacecraft operations as well as facilitates the modeling of the system with multiple levels of abstraction. The necessary primitives for the plan representation are defined. In hierarchical modeling using Petri nets, refinement is done by a compound (high-level) transition. A compound transition models either a complex activity, which corresponds to high-level operation on spacecraft or a method, which corresponds to the agent capability. At the lowest layer, a transition in the plan represents a primitive command to the spacecraft, such as ‘switch on camera’. The Petri net unfolding technique, which is a partial order approach, is applied to derive the plans from the dynamic knowledge models. This tackles the problem of combinatorial explosion. A hierarchical planning approach is followed, in which the abstract plan is recursively decomposed using the unfolding technique and refined by way of exercising the appropriate decisions in each layer. The reactive stratum is configured with three peer level agents. The control agent executes the command schedule and has the capability for reflex action. Structural properties of Petri nets are exploited by the execution-monitoring agent and the diagnostic agent for system level diagnosis. Fault tree method is applied for fine granularity diagnosis. The resultant architecture is a cost-effective solution, since it permits reusability of knowledge models across similar missions. The knowledge models are formally verified for ensuring the absence of deadlocks, buffer overflows, recoverability and detection of unreachable modules using Petri net properties such as reachability, liveness, boundedness, safeness, reversibility and home state. The high-risk components are subjected to safety property verification, which makes the system rugged. The hierarchical composition of Petri net models (which are independently verified), preserves liveness and boundedness characteristics and thus ensuring the reliability of the integrated models. This, in turn, ensures that reliable plans are generated on-board using these good quality models. The models of the system components viz. partial order plan, conditional plan, dynamic world model, reflex model, resource model and the hierarchical models are developed and demonstrated using HPSIM and Moses Tool Suite, using examples from spacecraft domain. The long-term planning agent, with hierarchical world models, for handling high-level goals is developed and simulated using Moses Tool Suite. The plan generation using unfolding approach is demonstrated using VIPTool, which has the partial order analysis capability. In summary, the main contributions include (a) Definition of a general framework for spacecraft autonomy; (b) design of a generic and reusable architecture for autonomous spacecraft using hybrid multi-agent concepts; (c) unified knowledge representation and reasoning using Petri nets across various strata/layers; (d) application of Petri net unfolding technique in a hierarchical manner for plan generation; (e) use of structural properties of Petri nets for fault identification and location; (f) verification and validation of Petri net models using Petri net properties and (g) simulation and demonstration of the system components viz. partial order plan, conditional plan, dynamic world model, reflex model, resource model and hierarchical models, by developing examples from spacecraft domain, using HPSIM and Moses Tool Suite and demonstration of plan generation using unfolding technique using VIPTool.

Les travaux de cette thèse portent sur l'analyse des comportements chaotiques dans les convertisseurs multicellulaires séries. Ces systèmes à commutationpeuvent présenter une variété de phénomènes complexes liés à des bifurcationset au chaos. Sachant qu'un convertisseur de puissance qui a une charge purementdissipative, ne peut générer un comportement chaotique, nous avons dans la première partie de cette thèse, connecté un hacheur à deux cellules à une charge non linéaire non strictement dissipative et nous avons analysé ses comportements à l'aide des propriétés dynamiques de base et présenté les routes vers le chaos. La fin de cette partie a été consacrée à l'étude du hacheur à cinq cellules qui est une généralisation du hacheur à deux cellules. Afin de supprimer le comportement chaotique, la deuxième partie du travail a été consacrée à la synthèse d'une loi de commande hybride basé sur la modélisation par réseaux de Petri pour la régulation des tensions des condensateurs flottants et du courant de charge. / This thesis deals with the analysis of chaotic behaviors in serial multicellularconverters. These switching systems can have a variety of complex phenomenaassociated with bifurcations and chaos. Knowing that a power converter that has a purely dissipative load cannot generate chaotic behavior, we've in the first part of this thesis, we connected a two-cell chopper to a nonlinear load not strictly dissipative and we've analyzed its behaviors by using some basic dynamic properties and thus presented the routes to chaos. The end of this part was devoted to the study of the 5-cell chopper which is a generalization of the two-cell chopper. In order to eliminate the chaotic behavior, the second part was devoted to the synthesis of a controlled law based on hybrid modeling of Petri nets for the regulation of capacitor voltages and current load.

O uso de técnicas e métodos formais contribui para o desenvolvimento de sistemas confiáveis. No entanto, apesar do rigor obtido, em geral, é necessário que essas técnicas sejam complementadas com atividades de teste e validação. Deve-se ressaltar que o custo para eliminar erros encontrados nas etapas iniciais de desenvolvimento é menor do que quando esses erros são encontrados nas fases posteriores. Dessa forma, é essencial a condução de atividades de VV&T - Verificação, Validação e Teste - desde as primeiras fases de desenvolvimento. Critérios de teste, como uma forma sistemática de avaliar e/ou gerar casos de teste de qualidade e, dessa forma, contribuir para aumentar a qualidade da atividade de teste, têm sido investigados para o teste de especificação de Sistemas Reativos. A técnica Redes de Petri Coloridas tem sido constantemente utilizada para a especificação do aspecto comportamental de Sistemas Reativos. Apesar de existirem diversas técnicas de análise, um aspecto não considerado é a cobertura alcançada, visto que, em geral, a aplicação exaustiva não é viável devido ao alto custo. Considerando a relevância do estabelecimento de métodos sistemáticos para o teste e validação dessas especificações, este trabalho propõe a aplicação do critério de teste Análise de Mutantes para o teste de Redes de Petri Coloridas. Neste trabalho foram almejados três objetivos principais, os quais podem ser divididos em estudos teóricos, estudos empíricos e automatização. No contexto de estudos teóricos, foi realizada a definição e embasamento teórico para possibilitar a aplicação da Análise de Mutantes no contexto de Redes de Petri Coloridas. Além disso, investigaram-se mecanismos genéricos para a descrição e geração de mutantes. Definiu-se um algoritmo para a geração de casos de teste baseado na Análise de Mutantes. No contexto de estudos empíricos, foram conduzidos estudos de caso para avaliar a aplicabilidade e eficácia dos resultados teóricos obtidos. Finalmente, no contexto de automatização, foram desenvolvidas ferramentas de apoio à aplicação da Análise de Mutantes. / The usage of formal methods and techniques contributes to the development of highly reliable system, but, in spite of the achieved rigour, these techniques must be complemented with testing and validation activities. It should be highlighted that the cost to eliminate errors found in the early phases of development is smaller than when those errors are found in the later phases. Therefore, the accomplishment of VV&T activities - Verification, Validation and Test - starting at the first development phases is essential. Testing criteria, as a systematic way to evaluate and/or generate test cases, contributing, therefore, to improve the quality of the test activity, have been proposed for testing reactive systems specifications. A technique that has been steadily employed for specifying the behavioural aspect of reactive systems is the coloured Petri nets. Although there are several analysis and validation techniques, a usually neglected aspect is the achieved coverage, given that, in general, the exhaustive application is not feasible due to its high cost. Considering the relevance of establishing systematic methods for the test and validation of coloured Petri nets based specification, this work proposes the investigation of the viability of applying Mutation Testing to test coloured Petri nets. In this work three main goals were pursued, which can be grouped in: theoretical studies, empirical studies and tool development. In the context of theoretical studies, it was accomplished the definition of theoretical concepts to enable the application of Mutant Analysis in the context of coloured Petri nets. Moreover, a mutation-based algorithm was defined to generate test sequences for Petri nets. In the context of empirical studies, case studies were carried out to evaluate the applicability and effectiveness of the achieved theoretical results. Finally, in the context of tool development, tools for supporting the application of Mutation Testing were developed.

Les systèmes d'alarmes jouent un rôle critique dans la bonne exploitation des installations industrielles modernes. Cependant, dans la plupart de ces systèmes, les alarmes ne sont pas toujours traitées correctement par les opérateurs car il y a régulièrement beaucoup trop d’alarmes à gérer, notamment lors des avalanches d’alarmes. Pour réduire le flux d'alarmes, notre approche consiste à détecter des redondances entre alarmes qui pourraient être supprimées. Pour atteindre cet objectif, nous recherchons dans un premier temps les adjacences fréquentes entre les alarmes contenues dans un historique. Ceci est réalisé en adaptant l’algorithme de recherche de motifs fréquents AprioriAll. Nous explorons également une seconde méthode consistant à trouver des précédences systématiques. Pour les découvrir, nous identifions les relations de domination et de mutuelle dépendance contenues dans l’historique des alarmes. Pour faciliter l’analyse experte, les relations découvertes sont traduites sous la forme d’un réseau de Pétri.Ces deux méthodes sont ensuite confrontées à un historique d’alarmes industriel fourni par General Electric. Les résultats obtenus montrent que nos deux méthodes permettent une réduction globale du flux d'alarmes qui est plus importante durant les avalanches. / Alarm systems play an important role for the safe and efficient operation of modern industrial plants. However, in most of industrial alarm systems, alarm flows cannot always be correctly managed by the operators as they often turn into alarm floods, sequences of numerous alarms occurring in a short period of time. To reduce the alarm flows, this report focuses on detection of redundant alarms that could be removed. This objective is met by, first, looking for frequent adjacency in the alarm log. To identify them, the frequent pattern mining algorithm AprioriAll is adapted. Another way to find potentially redundant alarms is to look for systematic predecessors. To discover them, dominations and mutual dependencies contained in the alarm log are identified. To ease this analysis, the discovered relations are depicted in the form of Petri nets.Both those methods are then tested against an industrial alarm log made available by General Electric. The results show that both methods allow a reduction of the alarm flow, with the biggest reduction being during alarm floods.

This master‘s thesis deals with the Deep Learning methods for image recognition tasks from the first methods to the modern ones. The main focus is on convolutional neural nets based models for classification, detection and image segmentation. These methods are used for practical implemetation – counting passing cars on video from traffic camera. After several test of available models, the YOLOv2 architecture was chosen and retrained on own dataset. The application also includes the addition of the SORT tracking algorithm.

This work deals with the development and use of a graphical editor of object-oriented Petri nets implemented in the PNtalk language. First, Petri nets that expand over time are described here. They are followed by a description of the object-oriented paradigm. Next, the structure of object-oriented Petri nets in the implementation of PNtalk is described here. Further work presents a description of the application design, which shows the entire structure of the application from the perspective of views. The main motivation for creating this tool is the effort to make object-oriented Petri nets accessible to their users. The application was implemented in the JavaFX framework and the whole procedure is given in the following chapter together with testing. The result of the work is presented in the examples contained in the last chapter, which also contains detailed manuals for controlling the application. The tool in cooperation with the PNtalk server enables users to work more pleasantly with OOPN and their visual appearance.

This diploma thesis deals with computer networks which play a key role in present society. More and more demands are placed on these networks (especially on quality of services and throughput) because of fast-growing developement of services such as voice and video real-time transmissions. All the packets in typical Ethernet networks are equal. Therefore it is sometimes impossible for the application to maintain required throughput speed of a network. For this case it is useful to take some mechanisms into the consideration. These mechanisms (sometimes called QoS) are able to distinguish different types of transmissions and traffic, analyze them and then prioritize them according to some pre-defined set of rules. The most famous mechanisms are Integrated Services and Differentiated Services. The implementation of Differentiated Services is the goal of this thesis.

This work is focusing on automatic verification of systems with parallel running processes. We discuss the existing methods and certain possibilities of optimizing them. Existing techniques are essentially based on finding an inductive invariant (for instance using a variant of counterexample-guided abstract refinement (CEGAR)). The effectiveness of these methods depends on the size of the invariant. In this thesis, we explored the possibility of improving the methods by focusing on finding invariants of minimal size. We implemented a tool that facilitates exploring the space of invariants of the system under scrutiny. Our experimental results show that many practical existing systems indeed have invariants that are much smaller than what can be found by the existing methods. The conjectures and the results of the work will serve as a basis of future research of an efficient method for finding small invariants of parallel systems.

This thesis deals with optimization problems of planning and scheduling. There are using genetic algorithms which are inspired by evolution process. Main work is familiar with the problem of planning and scheduling, genetic algorithm and Petri nets. This knowledge was used to create applications that would with the use of genetic algorithms was able to solve planning problems and the resulting plans would be represented the Time Petri Net. In conclusion of the this thesis are presented obtained results and examples of field use.

Le trafic ferroviaire urbain est quotidiennement sujet à des perturbations qui le dévient de son comportement nominal. Afin de minimiser l'impact de ces perturbations, les opérateurs ferroviaires usent de diverses techniques. Nonobstant leur efficacité, les performances de ces techniques ne sont généralement pas bien étudiées ni sont-elles optimales, car élaborées empiriquement. C'est dans ce cadre-ci que vient cet ouvrage fournir des solutions qui permettent d'évaluer ces techniques de régulation et d'en comparer les performances dans des contextes variés. L’approche proposée se base sur des variantes de réseaux de Petri comme modèles et sur la méthode de Monte-Carlo pour en simuler l’exécution. Cette combinaison a donné naissance à SIMSTORS, un outil de simulation pour les systèmes ferroviaires urbains, et plus généralement, pour les systèmes stochastiques régulés. Additionnellement, nous nous intéressons dans cette thèse à la problématique de la réalisabilité des tables horaires qui pilotent le trafic ferroviaire. Ces tables décrivent le comportement temporel désiré des systèmes pour lesquels elles sont conçues. Or, la construction de ces tables ne garantit pas toujours sa réalisabilité, notamment dans un contexte stochastique. Ainsi, nous proposons ici une méthode permettant de vérifier si une table horaire est bien réalisable avec une probabilité strictement positive. / Urban rail traffic is subject to numerous disrupting events that drift it from its nominal behavior. In order to minimize the impact of these disturbances, rail operators rely on a set of techniques. Despite their efficiency, performances of theses techniques are rarely well studied, nor are they of proven optimality; a direct consequence of them being empirically built. It is in this particular context that comes our work to provide solutions that allow for the evaluation of such techniques and for the comparison of their relative performances in various scenarios. The proposed approach is based on variants of Petri nets as models, and on the Monte-Carlo method for the simulation of their execution. This combination has led to the development of SIMSTORS, a tool for the simulation of urban rail systems, and more generally, stochastic systems under dynamic rescheduling. Additionally, this thesis addresses the question of timetable realizability; that is whether or not a given timetable is indeed realizable by a system for which it was built. Indeed, a timetable is meant to drive the behavior of a system but there is no guarantee as to its realizability. We therefore propose a method for the verification of the realizability of timetables with a strictly positive probability.