CoordenaÃÃo de AperfeiÃoamento de NÃvel Superior / Na conjuntura atual à possÃvel observar o grave problema de escassez energÃtica com o qual a humanidade se depara. Os derivados de petrÃleo estarÃo se exaurindo nas prÃximas dÃcadas e o tempo geolÃgico necessÃrio para a revitalizaÃÃo do estoque desta energia fÃssil a inviabiliza no longo prazo. Neste contexto, a busca por fontes renovÃveis de energia, como, por exemplo, o biodiesel, torna-se de suma importÃncia. Diversas oleaginosas podem ser empregadas para a produÃÃo de biodiesel, dentre as quais pode ser destacada a mamona. O agronegÃcio da mamona constitui-se numa cadeia produtiva complexa, tornando necessÃrios esforÃos dirigidos para a estruturaÃÃo desta cadeia ainda incipiente. Sistemas a Eventos Discretos (SED) vÃm sendo amplamente utilizados na modelagem de cadeias produtivas, apoiando o processo de planejamento e de gerenciamento de tais sistemas. Dentre as tÃcnicas de modelagem de SED, as redes de Petri destacam-se por propiciarem uma representaÃÃo compacta de um sistema e por permitirem a sua simulaÃÃo e anÃlise. O controle supervisÃrio de SED consiste em sintetizar um supervisor que coordene as atividades de subsistemas de modo que o sistema geral satisfaÃa um conjunto de especificaÃÃes. O objetivo geral deste trabalho foi elaborar um modelo, baseado em redes de Petri, que permitisse o controle supervisÃrio da Cadeia Produtiva do Biodiesel da Mamona (CP/BDMA), com vistas a garantir sua efetividade. Foi desenvolvido um novo mÃtodo de controle supervisÃrio baseado em redes de Petri coloridas, denominado RestriÃÃes de Controle sobre Cores Decompostas (RCCD), sendo tambÃm proposta uma arquitetura para o controle supervisÃrio em sistemas logÃsticos. Idealizou-se um modelo teÃrico da CP/BDMA no qual foi possÃvel ressaltar a importÃncia da coordenaÃÃo de atividades logÃsticas no Ãmbito da cadeia. Foram estabelecidas especificaÃÃes funcionais para o sistema e, em seguida, efetuou-se a avaliaÃÃo do seu desempenho, com base no tempo de ciclo, atravÃs da simulaÃÃo de diversos cenÃrios operacionais. Como conclusÃes, pode-se ressaltar que o mÃtodo RCCD constitui-se em uma eficiente abordagem para o controle de SED, que a modelagem proposta permitiu uma maior compreensÃo acerca do sistema em estudo e que o controle supervisÃrio à uma tÃcnica que pode subsidiar o processo de tomada de decisÃo no Ãmbito CP/BDMA, sendo tambÃm aplicÃvel a outras cadeias produtivas agroindustriais / Nowadays many countries present critical problems related to energy demand-supply equilibrium. The reserves of petroleum-based products are unable to face future demand for the next decades. So, the search for alternative sources of energy has been strongly directed to biodiesel. Several fruit oils can be used as a source for biodiesel production and the castor bean is an example. The castor bean agribusiness is a complex commodity chain, making necessary researches for the conception of this incipient chain. Discrete Event Systems (DES) are largely used in the modeling of commodity chains, aiding the planning and the manage of these systems. Among the DES modeling techniques, the Petri nets stands out for as making a easier a compact representation of a system and for permitting its simulation and analysis. The supervisory control aims for synthesize a supervisor that coordinate the activities of the subsystems in order to satisfy a set of specifications in a general system. The general purpose of this work was create a model, based on Petri nets, that permit the supervisory control of Castor Bean Biodiesel Supply Chain (CBB/SC) in order to guarantee its efficiency and efficacy. It was developed a new method for the supervisory control based on colored Petri nets, called Constraints of Control on Decomposed Colors (CCDC). Also, it was proposed a new framework for the supervisory control in logistics systems. Functional specifications were established for found the system which had its performance evaluated, based on the lead time, through simulation of several operational scenarios. As conclusion, it seems clear that the CCDC method is a consistent approach for DES control, the proposed model helps in a better comprehension about the system in analysis and the supervisory control is a theory that can aid the decision making process in similar chains as CBB/SC

Made available in DSpace on 2015-04-11T14:03:15Z (GMT). No. of bitstreams: 1 DISSERTACAO MARCELO.pdf: 1313111 bytes, checksum: ddf9a22433355413e807d3bd27951a01 (MD5) Previous issue date: 2008-12-15 / Fundação de Amparo à Pesquisa do Estado do Amazonas / Embedded systems have undeniable relevance in modern society. They have temporal constraints (as long as they are real time ones), power consumption management, size, weight, etc which make their design more complex than the design of their desktop peers. Given the huge number of requirements of all kinds, the high complexity of embedded software as well as the big possibilities of critical damages in case of flaws and, at last, the even bigger pressure of market for new products faster, it make necessary methods which can assure correct, fast but intuitive specification and conception of designs. Considering this, this work aims to provide a method which contribute to the state of art. The goal of the proposed method is to provide an approach which gather an specification of an embedded software in a semi-formal, object-oriented and Industry-accepted notation, which is Unified Modeling (UML), specifically their Sequence Diagram notation which is able to capture dynamic aspects of a system and a mecanism of translation of this notation into a formal one, called SMV, apropriate for being used by the SMV model checker. The goal of the method is also provide an translation scheme of the sequence diagrams into another formal notation, the so called Petri Nets notations. Petri Net notation is well suited to formal verification. Finally, the goal of the method is to provide a mechanism of translation of high level properties queries into formal notation CTL. Property queries are only qualitative. All these functionalities are implemented in a tool called Ambiente de Verificação Formal de Software Embarcado. / Os sistemas embarcados possuem inegável importância na sociedade atual. Eles possuem restrições temporais (quando são de tempo real), de gerência de consumo de energia, tamanho, peso etc que tornam o seu projeto e concepção mais complexos do que os sistemas convencionais. Dado o grande número de requisitos de todos os tipos, a alta complexidade dos softwares embarcados desenvolvidos bem como a grande possibilidade de catástrofes significativas em caso de falha e por fim a grande pressão de mercado por produtos cada vez mais rápido, fazem-se necessários métodos que possam assegurar uma correta, rápida porém intuitiva especificação e concepção dos projetos. Diante disso, o presente trabalho visa prover um método que acrescente ao atual estado da arte. O objetivo do método então é prover uma abordagem que colete uma especificação de software embarcado em uma notação semi-formal, orientada a objetos e amplamente aceita pela Indústria, que é a Unified Modeling Language (UML), especificamente com seu Diagrama de Sequência, o qual é apto para capturar os aspectos dinâmicos de um sistema e um mecanismo de tradução dessa notação para a notação formal SMV, apta a ser utilizada pelo model checker de mesmo nome. O objetivo do método é prover também um esquema de tradução dos diagramas de sequência em UML para uma notação formal, no caso a notação de Redes de Petri, o qual é adequada para verificação formal, gerando saídas de arquivos nos formatos APNN e PNML. O formato APNN é adequado para ser usado no Model Checking Kit (MCK). Por fim, prover um esquema de tradução consultas de propriedade em alto nível para o formato de CTL puro adequado para ser usado no MCK e um programa em SMV e sua especificação 7 em CTL, formatos aptos a serem usados no model checker SMV. A verificação de propriedades é apenas qualitativa, isto é, que verificará apenas propriedades de execução do software embarcado, em oposição às propriedades quantitativas de tempo por exemplo, comuns em softwares de tempo-real. Todas essas funcionalidades são realizadas por uma ferramenta, chamada Ambiente de Verificação Formal de Software Embarcado.

Os modernos sistemas de mediÃÃo, proteÃÃo, comando, controle e supervisÃo (MPCCS) tÃm contribuÃdo de forma significativa para o aumento da seguranÃa, confiabilidade e continuidade de serviÃo dos sistemas elÃtricos de potÃncia. O sistema de proteÃÃo à parte relevante desse sistema multifuncional, o qual tem como objetivo principal manter a integridade do sistema elÃtrico quando submetido a um distÃrbio, garantindo a seguranÃa de pessoas e assegurando a continuidade de serviÃo da porÃÃo nÃo envolvida no problema. Para tanto, o sistema de proteÃÃo deve atender a alguns requisitos bÃsicos tais como: boa seletividade e coordenaÃÃo, rapidez na atuaÃÃo, sensibilidade para proteger a maior zona de proteÃÃo possÃvel e confiabilidade. No sistema de proteÃÃo, um componente assume uma posiÃÃo de destaque: o relà de proteÃÃo digital. à neste componente que sÃo configurados os ajustes necessÃrios para o correto funcionamento do esquema de proteÃÃo de um dado sistema elÃtrico. Os relÃs de proteÃÃo digitais sÃo equipamentos multifuncionais, que possuem diversas funÃÃes de proteÃÃo, mediÃÃo de grandezas elÃtricas, registros oscilogrÃficos, supervisÃo, controle e comunicaÃÃo. AlÃm de todos estes recursos, os relÃs digitais dispÃem de mÃltiplos grupos de ajustes que podem ser previamente configurados conforme necessidade operacional. A mudanÃa de grupo de ajuste de um relà à um recurso amplamente utilizado pelas Ãreas de proteÃÃo das empresas do setor elÃtrico, possibilitando uma otimizaÃÃo do ajuste do sistema de proteÃÃo, compatibilizando-o Ãs diversas topologias assumidas pelo sistema elÃtrico apÃs uma falta ou retirada intencional de algum componente da rede. Atualmente este procedimento à realizado de forma manual, tornando-o vulnerÃvel à falha humana, podendo ter como consequÃncia desligamentos de grandes blocos de carga por falha de coordenaÃÃo, com graves prejuÃzos para os indicadores da qualidade de serviÃo de duraÃÃo e frequÃncia de interrupÃÃo, DEC e FEC, e para a imagem da empresa. Neste trabalho à apresentado um sistema, baseado em Redes de Petri Coloridas, capaz de realizar a mudanÃa automÃtica entre grupos de ajustes de um sistema de proteÃÃo a partir da mudanÃa de topologia do sistema elÃtrico. O sistema desenvolvido monitora a topologia da rede elÃtrica, em tempo real, a partir das informaÃÃes de estado dos disjuntores. Para qualquer alteraÃÃo na configuraÃÃo da rede elÃtrica, que caracterize necessidade de alteraÃÃo no sistema de proteÃÃo, automaticamente sÃo enviados sinais de comando para os relÃs, alterando os grupos de ajustes ativos de um conjunto predefinido, de modo a se obter a melhor graduaÃÃo de proteÃÃo possÃvel para a porÃÃo correspondente do sistema elÃtrico afetado pela alteraÃÃo de topologia. / The modern systems of measurement, protection, command, control and supervision (MPCCS) have contributed in a meaningful way to increase the security and reliability of the power systems. The most important part of this multifunctional system is the protection system, which has as the main goal to maintain the power system integrity when it is under a disturbance, assuring the peopleâs safety as well as the continuation of the services to the part of the system not involved in the disturbance. For this, the protection system must fulfill some basic requirements such as: proper selectivity and coordination, prompt response, sensitivity to protect the largest zone as possible and reliability. In a system protection, one component takes on a prominent position, given its functional importance: the digital protection relay. It is in this device where the necessary adjustments are configured for proper operation of the protection scheme of a given electrical power system. The digital relays are devices that have several protection functions, with multiple levels of settings, measurements, oscillography, supervision, control and communication. Besides all these features, the digital relays have multiple groups of settings that can be previously configured and switched among them, according to operational needs. The changing of setting group in a relay is a very important resource at a protection system, extensively used by protection sectors of companies in the power sector, allowing the optimization of the protection system setting, making it compatible to a new topology taken on by the system after a fault or an intentional removal of some system component. Nowadays this procedure is performed manually, making it vulnerable to human errors that might occur as a consequence of an outage, with serious effect in the system performance indices. In this sense this work presents a system, based on Colored Petri Nets, able to automatically change the setting groups of a protection system when the power network topology changes. This system monitors in real time the status of the circuit breakers in order to take the decision whether a meaningful change in the network topology has taken place. If so, a command is automatically sent to the relays to change the active group setting so as to maintain a suitable coordination of the protection system.

Atualmente, sabe-se que grande parte dos acidentes graves ocorridos envolvendo uma diversidade de sistemas como plataformas de petróleo, aeronaves ou plantas de processos industriais, poderiam ser evitados caso possuíssem dispositivos de controle projetados especificamente para manter a segurança durante a ocorrência de falhas no funcionamento dos mesmos. Por outro lado, observam-se complicações em realizar o controle de sistemas remotos em que é possível não haver garantia de monitoração em tempo real, como o caso de sondas espaciais ou robôs de exploração. Neste contexto, podem-se encontrar ambas as dificuldades no controle do funcionamento de um Dispositivo de Assistência Ventricular (DAV) que desempenha a função de auxiliar o bombeamento de sangue para o sistema circulatório de um paciente com insuficiência cardíaca. Este tipo de dispositivo, quando usado para terapia de destino, deve apresentar um elevado nível de segurança, pois, caso haja falha, o risco de morte é eminente. Por sua vez, o sistema deve apresentar um elevado índice de autonomia, já que as características comportamentais e fisiológicas de um paciente estão em constante mudança e afetam diretamente o modo como deve ocorrer a interação entre o DAV e o sistema cardiovascular do paciente. Sendo assim, há uma necessidade premente de aprimoramento do projeto de sistemas de controle de DAVs autônomos e seguros. A proposta do presente trabalho consiste em aplicar conceitos mecatrônicos para o projeto de um sistema de controle de DAVs e, considerando a natureza dos sinais que indicam a ocorrência de falhas, considerar a teoria de Sistemas a Eventos Discretos (SED), ferramentas de análise de risco e técnicas de diagnóstico e tratamento de falhas para a obtenção de modelos de controle considerando-se uma arquitetura modular e distribuída. Desta forma, foi desenvolvida uma arquitetura de controle supervisório para DAVs considerando características de variações de comportamento do sistema circulatório do paciente e do próprio DAV. Esta arquitetura de controle contempla o diagnóstico e tratamento de falhas desenvolvendo um método para a classificação de falhas e, de acordo com a severidade de cada uma delas é proposto um sistema de controle que atua na regeneração ou degeneração do DAV para um estado seguro, v observando, também, o cumprimento de normas médicas e técnicas de segurança. Para atingir este objetivo, propõe-se uma sistemática para o projeto do sistema de controle para DAVs considerando o aspecto multidisciplinar pertinente a este contexto. A base dessa sistemática consiste em realizar uma efetiva análise de risco do sistema utilizando a ferramenta de estudo HAZOP (Hazard and Operability Studies). A partir do conhecimento obtido sobre o comportamento do sistema em situações críticas desenvolvem-se modelos formais utilizando rede Bayesiana e rede de Petri para o diagnóstico e tratamento das possíveis falhas. O comportamento do DAV controlado pode ser analisado de duas formas: (i) a partir de ensaios in vitro utilizando técnicas de análise por simulação e ferramentas computacionais adequadas, além de testes em simuladores cardiovasculares físicos que emulam interação com o sistema circulatório humano; (ii) a partir de ensaios in vivo em animais que poderão ser utilizados para simular modelos físicos de insuficiência cardíaca e permitir uma avaliação fidedigna dos efeitos do implante do DAV. O procedimento proposto foi aplicado para um caso real de desenvolvimento de um DAV envolvendo uma equipe de pesquisadores da Escola Politécnica da USP e do Instituto Dante Pazanesse de Cardiologia. Assim, é possível obter-se um sistema de controle autônomo e seguro que atenda normas técnicas aderentes a esse assunto e os rigorosos requisitos de projeto impostos a essa classe de sistema. / Nowadays, it is kwon that the several of severe disasters compromising a great variety of systems such as oil platforms, aircrafts or industrial plants, could have been avoided if these systems had controllers designed specifically to maintain the safety levels in case of fault. On the other side, many complications are observed on performing the control of remote systems, where there is no guarantee of real time monitoring of the system, as in space probes or reconnaissance robots. In this context, both obstacles can be found on the control of ventricular assist devices (VAD), which have the role of assisting to pump the blood into the patients circulatory system, in case of irregular heartbeat or heart failure. Devices such as the VAD must possess very high safety levels, as in case of fault, the consequences are severe and might result on the dead of the patient. Nevertheless, these systems must have high degree of autonomy, as the patients physiology and behavior are constantly changing, and these changes impact directly the interactions between the VAD and the patient´s cardiovascular system. Thus, there is a pressing need to improve the design of safe and autonomous control systems for VADs. The present work proposes applying mechatronic concepts to the development of control systems for VADs, considering the nature of the fault indicating signals, as well as the Discrete Event Systems (DES) theory and through the application of tools for risk analysis, and fault diagnostic and treatment techniques aiming the development of control models based on modular and distributed architectures. Thereby, a VAD supervisory control architecture was developed, where the behavior variations of the patient´s circulatory system as well as of the VAD were taken into consideration. This control architecture features the diagnostic and treatment of faults, where methods for faults classification where developed, and according to the severity each fault is proposed a control system that performs the regeneration or degeneration of the VAD to a secure state and is according to medical standards and safety techniques. To achieve this goal is proposed a systematic for the design of the VAD control system considering the multidisciplinary context of the device. The foundation of this systematic is the performance of an effective risk analysis through the use of the toolset known vii as HAZOP (Hazard and Operability Studies). From the knowledge acquired about the system behavior during critical conditions, formal models are developed employing Bayesian Networks and Petri Nets for the diagnostic and treatment of faults. The behavior of the controlled VAD can be analyzed in two possible ways: (i) from in vitro experiments, through the use of simulation analysis tools and proper computational tools, as well as tests on real cardiovascular simulators, where the interactions between the VAD and the human circulatory system can be emulated; (ii) from in vivo experiments, animals can be used to simulate physical models of irregular heartbeat or heart failure and allow reliable valuations of the VAD implant. The proposed procedure was applied on the VAD development, which was performed by a team of researchers from the Escola Politécnica da USP and from the Instituto Dante Pazanesse de Cardiologia. Thus, is possible to achieve an autonomous and safe control system that complies with the applicable technical standards, as well as the strict project requirements for this class of system.

Orientador: Furio Damiani / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Elétrica e de Computação / Made available in DSpace on 2018-08-21T16:34:47Z (GMT). No. of bitstreams: 1 Dezani_Henrique_D.pdf: 4299449 bytes, checksum: 739b593ddd96b9124b1882d5510a0ce0 (MD5) Previous issue date: 2012 / Resumo: O controle do tráfego urbano constitui um importante tópico de pesquisa nos dias atuais. De fato, a cada dia aumenta a quantidade de veículos trafegando nas vias urbanas, as quais nem sempre são modificadas para a melhoria do tráfego. A existência de transportes públicos também não resolve o problema, visto que estes disputam o espaço nas vias com os demais veículos. Na literatura, foram encontrados diversos trabalhos que tentam resolver este problema reajustando o tempo semafórico das interseções ou, de maneira isolada, definindo rotas para um veículo. Neste projeto é apresentada uma nova maneira de abordar o problema, por meio do desenvolvimento de um sistema que otimiza o fluxo do tráfego urbano, em tempo real, ao explorar as possíveis rotas para cada veículo trafegando em uma determinada área urbana, utilizando análises em rede de Petri, e, então, a partir de um Algoritmo Genético, definir as rotas que diminuam o tempo e/ou tamanho das filas formadas nestas vias. Ainda neste trabalho, diversos testes são efetuados sobre o sistema desenvolvido, comprovando sua eficiência em relação às técnicas existentes / Abstract: Urban traffic control is an important research topic in the present days. In fact, everyday, the amount of vehicles traveling on urban roads increases. Moreover, such roads are not always modified for traffic improvement. Also, the availability of public transportation does not solve the problem, since they compete for space on the roads with other vehicles. Several papers have been found in the literature that attempt to solve this problem by either readjusting the traffic light time in intersections or isolately defining routes for a vehicle . This thesis presents a new way to approach the problem through the development of a system that optimizes the urban traffic stream, in real time, exploring possible routes for each vehicle traveling on a given urban area using Petri net analysis, and then, with a Genetic Algorithm, defines routes which reduce the time and/or size of the queues formed in such lanes. Also in this work, several tests are performed on the developed system, proving its efficiency with respect to existing techniques / Doutorado / Eletrônica, Microeletrônica e Optoeletrônica / Doutor em Engenharia Elétrica

Orientadores: Norian Marranghello / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-08-04T00:21:09Z (GMT). No. of bitstreams: 1 Oliveira_WagnerLuizAlvesde_D.pdf: 11239313 bytes, checksum: 6656f5270142e68410f7ed92ce02dc2d (MD5) Previous issue date: 2004 / Resumo: O projeto de sistemas digitais alcançou um elevado grau de complexidade, inviabilizando sua consecução sem o uso de ferramentas de CAD. O ponto de partida de tais ferramentas consiste numa visão conceitual do sistema pretendido (dada por um ou mais modelos conceituais), a qual é capturada para tratamento computacional por uma ou mais linguagens de especificação. Várias dessas linguagens foram desenvolvidas visando capturar tantas características de hardware e de software quanto possível, de acordo com diferentes metodologias de projeto. Rede de Petri é uma classe de modelos conceituais utilizada na modelagem de diversos tipos de sistemas computacionais paralelos. Algumas extensões de rede de Petri foram propostas visando à descrição, de forma tão acurada quanto possível, de características de sistemas digitais. Entretanto, somente duas destas extensões possuem um número maior de características necessárias à descrição integral de tais sistemas. O presente trabalho apresenta uma extensão de rede de Petri desenvolvida para superar as limitações das demais extensões na representação de sistemas digitais. O trabalho apresenta, também, uma metodologia de coprojeto hardware/software na qual a extensão proposta pode ser usada como linguagem de modelagem interna. Tal plataforma visa a descrição, simulação, análise, validação e síntese em alto nível de sistemas digitais embutidos / Abstract: Digital system design has reached a high degree of complexity that prevents its realization without CAD tools. The starting point of such tools consists on a conceptual view of the intended system (given by one or more conceptual models), which is captured for computational handling by one or more specification languages. Several of such languages were developed aiming to capture as many hardware and software characteristics as possible, according to different design methodologies. Petri net is a class of conceptual models for parallel system modeling. Some Petri net extensions have been proposed aiming at describing digital systems characteristics as accurately as possible. However, only two of them have nearly all features needed to describe such systems in full. This work presents a Petri net extension developed to overcome the restrictions for digital system modeling through Petri net extensions. A hardware/software codesign methodology in which the proposed extension can be used as the internal modeling language is presented as well. Such a framework aims embedded digital system description, simulation, analysis, validation, and high-level synthesis / Doutorado / Eletrônica, Microeletrônica e Optoeletrônica / Doutor em Engenharia Elétrica

Context. Name-bounded analysis is a type of static analysis that allows us to take a concurrent program, abstract away from it, and check for some interesting properties, such as deadlock-freedom, or watching the propagation of variables across different components or layers of the system. Objectives. In this study we investigate the difficulties of giving a representation of computer programs in a name-bounded variation of π-calculus. Methods. A preliminary literature review is conducted to assess the presence (or lack thereof) of other successful translations from real-world programming languages to π-calculus, as well for the presence of relevant prior art in the modelling of concurrent systems. Results. This thesis gives a novel translation going from a relevant subset of the Java programming language, to its corresponding name-bounded π-calculus equivalent. In particular, the strengths of our translation are being able to dispose of names representing inactive objects when there are no circular references, and a transparent handling of polymorphism and dynamic method resolution. The resulting processes can then be further transformed into their Petri-Net representation, enabling us to check for important properties, such as reachability and coverability of program states. Conclusions. We conclude that some important properties that are not, in general, easy to check for concurrent programs, can be in fact be feasibly determined by giving a more constrained model in π-calculus first, and as Petri Nets afterwards. / +49 151 52966429

Cette thèse concerne l'élaboration de stratégies de commande prédictive pour certaines classes de systèmes dynamiques continus, discrets et hybrides modélisés par des extensions de réseaux de Petri ad hoc. Pour les systèmes continus et en vue de limiter la complexité de calcul inhérente à la forme standard de la commande prédictive, plusieurs améliorations sont proposées. Celles-ci permettent de surmonter le problème de "hill climbing" caractéristique des trajectoires obtenues avec certains réseaux de Petri. Elles assurent également la possibilité d'implémenter la commande en temps réel en adaptant l'horizon de prédiction pour réduire la complexité algorithmique. Enfin, elles permettent de limiter la sollicitation des actionneurs tout en garantissant la stabilité asymptotique du système commandé. Pour les systèmes discrets temporisés et pour éviter l'exploration exhaustive du graphe d'atteignabilité, une méthode de commande est proposée, basée sur la commande prédictive appliquée à une approximation continue du système discret. Enfin pour les systèmes hybrides, une commande prédictive hybride est développée, inspirée de la commande prédictive continue. Les performances de ces différentes stratégies de commande sont évaluées et comparées avec différentes simulations numériques / This thesis concerns the development of predictive control strategies for some classes of continuous, discrete and hybrid dynamic systems modeled by specific extensions of Petri nets. For continuous systems and in order to limit the computational complexity inherent to the standard form of the predictive control, several improvements are proposed. These improvements allow overcoming the problem of hill climbing that characterizes trajectories obtained with some Petri nets. They also ensure the possibility to implement real-time control by adapting the prediction horizon in order to reduce the algorithmic complexity. Finally, they limit actuators solicitation while ensuring the asymptotic stability of the controlled system. For timed discrete systems and in order to avoid the exhaustive exploration of the reachability graph, a control method is proposed, based on the predictive control applied to a continuous approximation of the discrete system. Finally for hybrid systems, hybrid predictive control is developed, inspired by the continuous predictive control. The performance of these different control strategies are evaluated and compared to different numerical simulations.

Les MSG (pour « Message Sequence Graphs ») sont un formalisme bien connu et souvent utilisé pour décrire des ensembles de scénarios de manière visuelle dans le domaine des protocoles de communication. Nous nous intéressons dans la première partie de la thèse à la détection de la divergence, la vérification de la coopération globale ainsi que la vérification de propriétés d’accessibilité et de couverture. Notre première contribution consiste à utiliser des solveurs SAT afin de résoudre ces problèmes efficacement. Afin de munir le formalisme des MSG de compteurs, de timers et d’autres aspects, nous introduisons le modèle des PNS (pour « réseaux de Petri avec états ») et une sémantique de processus non-branchants. Ce modèle est non seulement plus expressif que les MSG, mais il permet également des spécifications plus concises. Nous nous intéressons à trois problèmes de vérification classiques sur l’ensemble des marquages accessibles par les préfixes des processus : le caractère borné, la couverture et l’accessibilité. Afin de considérer des systèmes paramétrés, nous introduisons également la notion de borne semi-structurelle. Cela consiste à fixer le marquage initial d’un sous-ensemble approprié de places, puis à vérifier que le système est borné, quelles que soient les valeurs des paramètres. Nous montrons comment un dépliage conduit à un problème plus simple à vérifier. Une caractéristique particulièrement attrayante des MSG et des PNS réside dans leur représentation graphique similaire à un automate. Il est donc intéressant de décrire les bugs de manière visuelle. Nous montrons comment calculer en temps polynomial une représentation simple et concise d’un bug. / Message Sequence Charts (MSCs) are a popular model often used for the docu- mentation of telecommunication protocols. In the first part of the thesis, we focus on detecting process divergence, checking global-cooperation and checking reachability properties. Our first contribution is to use SAT solvers to solve these problems effectively. In order to study MSC specifications with counters, timers and other features, we introduce the model of Petri nets with states together with a non-branching non-sequential process seman- tics. We obtain a framework that is more expressive and more concise than MSGs. We consider then three classical verification problems for the set of markings reached by prefixes of processes : boundedness, covering and reachability. We consider also the notion of semi-structural property in order to study parametrized sys- tems. In this way, only part of the places are provided with an initial marking. Unfolding such a system leads to a simpler problem in the form of a linear programme. A particularly attractive feature of MSG and PNS lies in their graphical representation similar to an automaton. So, it is interesting to describe the bugs visually. We show how to compute in polynomial time a simple and concise representation of a bug.

This thesis focuses on Internet of Things (IoT) and open-source technologies based on it. Specifically aims at software solutions relevant to smart home and compatible with Raspberry Pi platform and MQTT communication protocol. This thesis also focuses on studying Petri Net Virtual Machine (PNVM) and its potential application in IoT. The objective is to design integration of PNVM into IoT with help of existing software means compatible with MQTT and implement a demo application for smart home.