O presente trabalho trata da verificação e design de sistemas complexos, especificamente da verificação de sistemas de tempo real concorrentes e distribuídos. Propõe-se uma técnica enumerativa para a verificação formal de modelos que permite determinar a validade de propriedades quantitativas, além das qualitativas. A técnica proposta separa a construção do espaço de estados dos algoritmos de rotulação das fórmulas temporais, o que possibilita a diminuição da complexidade do processo de verificação, tornando-o viável para aplicações práticas. A técnica proposta foi inicialmente aplicada sobre modelos de redes de Petri temporizadas e depois em uma rede unificada chamada GHENeSys para aproveitar as características de abstração, hierarquia e de elementos de interação chamados pseudo-boxes. A definição da rede GHENeSys foi modificada para permitir a modelagem de sistemas onde os requisitos temporais devem ser expressos através de atrasos e prazos como e o caso dos sistemas de tempo real. A rede suporta ainda mecanismos de refinamento tanto para os elementos ativos quanto os passivos. A demonstração da manutenção de propriedades como invariantes, vivacidade, limitação assim como da validade de fórmulas lógicas no processo de refinamento constitui um aspecto fundamental no projeto de sistemas complexos, e foi portanto revista em detalhes para a rede GHENeSys. Alguns exemplos práticos são apresentados para avaliar o desempenho dos algoritmos e um estudo de caso finaliza a apresentação, onde se pode contrastar os algoritmos propostos com os implementados na ferramenta UPPAAL. / This work deals with the process of design and verification of complex systems, mainly real time, concurrent and distributed systems. An enumerative technique is proposed for model-checking which is capable of determining both quantitative and qualitative properties. The proposed technique detach the algorithm for labeling the formula being checked from the state space construction, allowing a better result in the verification process. This model-checking approach shows itself valuable in practical applications. This approach was first applied to systems modeled by Time Petri Nets and further extended to a unified net called GHENeSys, which includes abstraction and hierarchy concepts as well as elements for data and control interchange, called pseudo-boxes. The GHENeSys definition was modified in order to deal with systems in which temporal requirements can be expressed through delays and deadlines as in the real-time systems. The GHENeSys environment supports a refinement technique applied to both passive and active elements. Net properties like invariants, liveness, boundedness and also the validity of temporal formulas was proved to be maintained through the refinement process if some conditions are satisfied. Such characteristics are useful to deal with complex systems design. Some experiments based on well known academic articles were used to avaliate the performance of the algorithms and a case study is presented in order to compare obtained results with those obtained using the UPPAAL tool.

As tecnologias da informação, telecomunicações e mobilidade aliadas às mudanças econômicas e sociais acarretaram uma grande reestruturação da indústria. Entre estas mudanças, verifica-se um maior nível de descentralização e especialização das unidades produtivas, o aumento da automação dos processos e, em conseqüência, uma maior quantidade e complexidade nas interações de seus sub-sistemas. De forma a lidar com esta complexidade e facilitar o estudo e projeto de novos sistemas, faz-se necessário o uso de modelos, que são analisados por exemplo, através de simulação. Entre elas destaca-se a simulação distribuída, a qual trata da evolução de situações/cenários do sistema em computadores fisicamente dispersos, conectados através de uma rede de comunicação, visando, por exemplo, a redução do tempo de simulação, a simulação de grandes modelos(composto por muitos elementos), maior tolerânica a falhas e mesmo a distribuição geográfica. Visando contribuir para uma maior aplicabilidade das técnicas de modelagem e simulação, em especial a distribuída, propõe-se nesta tese (1) um novo método para a modelagem hierárquica de sistemas produtivos; e (2) um novo algoritmo para a sincronização da evolução do tempo de simulação de diferentes simuladores interagindo através de redes de comunicação (LAN, WAN). No método de modelagem proposto, utiliza-se uma abordagem top-down para a decomposição do sistema, partindo-se de um nível de abstração para um de maior detalhamento, permitindo, assim, um maior nível de conhecimento quanto ao comportamento dos elementos e suas interações. No nível de detalhamento desejado, utiliza-se a Rede de Petri na modelagem dos elementos básicos do sistema, que são, assim como na orientação a objetos, denominados classes. Em seguida, através de uma abordagem bottom-up, estes modelos são agrupados, formando modelos mais complexos: componentes e aplicativos. A fim de garantir a interação entre estes elementos, foram definidos um conjunto de interfaces, bem como suas regras de relacionamento. Este método foi aplicado a um estudo de caso para comprovar sua eficácia. No que diz respeito ao algoritmo proposto para sincronizar os tempos de simulação, utiliza-se como subsidio o mecanismo de gerenciamento da transmissão de dados em redes conhecido como Token Ring. Um simulador de eventos, distribuído, foi implementado com a finalidade de validar o algoritmo proposto. / Evolution on the information technology, telecommunications and transport systems, associated to social and economic changes around the world have caused a significative reorganization of the industry. In this context, a high level of decentralization and specialization of the productive units, as well as an increment of the automation level used in productive processes have been verified. It results on the increase of the amount and the complexity of the enterprise subsystems interactions. Modeling techniques are used with simulation to deal with the complexity, to analysis, and to design new productive systems. Among the simulation approaches, distributed simulation is distinguished. It deals with the execution of simulation in physically dispersed computers connected through a LAN (Local Area Network), providing, for example, the reduction of the simulation time, huge simulation models (models with many elements), fault tolerance, as well as geographic dispersion. To contribute for the evolution of modeling and simulation techniques, in special the distributed one, it is proposed on this work: (1) a new method for the hierarchical modeling of productive systems; and (2) a new time synchronization algorithm used to manage the time evolution of a set of distributed simulation software. On the proposed modeling method it is used a top-down approach to decompose the system in basic elements, starting in a high-level abstraction model, and ending with a set of basic models with high level of detail. Then, these models are modeled using Petri net. As well as on object-oriented languages, each model is called class. After that, using a bottom-up approach, these basic models are grouped to generate more complex models: component and application. A set of interfaces, as well as its relationship rules had been defined to guarantee the interaction among these elements. This method was applied to a case study to confirm its effectiveness. About the time synchronization algorithm, the token ring protocol is used as subsidy. An event based distributed simulator was implemented with the purpose to validate the proposed algorithm.

Dentro do conceito de "Edifício Inteligente", que tem como objetivo a otimização da infra-estrutura física e do ambiente em relação a aspectos de produtividade e comportamentais, este trabalho apresenta uma metodologia para modelagem e simulação de estratégias de gerenciamento de sistemas de ar condicionado onde focaliza-se a integração do ar condicionado com os demais sistemas de um edifício. Para tanto introduz-se uma abordagem híbrida onde são considerados aspectos de Sistemas a Eventos Discretos e de Sistemas de Variáveis Contínuas. Como estudo de caso apresenta-se a modelagem do sistema de ar condicionado do Prédio dos Ambulatórios do Hospital das Clínicas da Faculdade de Medicina de São Paulo, para o qual se aplica o método proposto para análise do tratamento de perturbações no sistema de ar condicionado resultantes de variações da carga térmica. / Considering "Intelligent Buildings", which have as one of its purpose to improve its structure and environment in order maximise the effectiveness of its occupants, this work introduce a methodology for modelling and simulation of HVAC systems. The focus is on the integration of the HVAC system with other building systems. A hybrid approach is introduced to consider both discrete and continuous aspects. As case study, we present the models for the Ambulatory Building of Hospital of the Medical School of São Paulo University. Particularly, the proposed methodology is used to analyse if the response of the HVAC system to thermal load variations can be enhanced, improving the thermal comfort, when integration between systems is considered.

O sistema de elevadores como equipamento para o transporte vertical de pessoas e bens é um componente fundamental no projeto de edifícios e, neste âmbito, a disponibilidade e eficiência do seu serviço deve ser objeto de cuidadosa análise em função de sua influência no desempenho e produtividade das atividades dos usuários do prédio. Neste contexto e considerando especificamente os edifícios inteligentes cuja finalidade é a otimização a nível estrutural e funcional do edifício como um todo, e onde a integração entre seus sistemas cumpre um papel fundamental para atingir estes objetivos, o presente trabalho propõe uma metodologia para a modelagem de sistemas de elevadores nestes prédios, que considera a sua integração com outros sistemas prediais. A abordagem empregada no desenvolvimento deste trabalho baseia-se na caracterização dos sistemas de elevadores como sistemas a eventos discretos (SED), pois sua dinâmica é definida através da ocorrência de eventos e a manutenção de estados discretos. Assim, na metodologia utiliza-se técnicas derivadas das redes de Petri (redes de Petri interpretadas), de comprovada eficiência para a modelagem, análise e controle de SEDs. Estas ferramentas são usadas através de uma abordagem estrutural, onde o sistema é modelado em diferentes níveis de abstração: um modelo conceitual obtido pelo uso da técnica PFS (Production Flow Schema) em um primeiro nível, e o refinamento deste para modelos funcionais através do uso do MFG (Mark Flow Graph) e suas extensões, onde são preservadas as estruturas das atividades do nível superior e são descritos os detalhes em um nível funcional. A metodologia proposta confirmou ser útil e eficiente para a modelagem do sistema de elevadores em edifícios inteligentes, ao permitir a especificação do modelo funcional de todo o sistema (objeto de controle e sistema de controle) e das estratégias que facilitam a sua integração com outros sistemas prediais / The elevator system as mean for the vertical transport of people and goods is a fundamental component in the design of buildings. The availability and efficiency of this service must be object of careful analysis due to its influence on the performance and productivity of the building users' activities. In intelligent buildings, the purpose is the optimization of its structural and functional levels and where also the integration between all building systems accomplishes a fundamental role to reach these objectives. In this context, this work proposes a methodology for the modeling of elevator systems in these buildings, which consider your integration with others buildings systems. The approach developed in this work is based on the characterization of elevator systems as Discrete Event Systems (DES), since the dynamic behavior is defined through the discrete events and discrete states. The proposed methodology uses techniques, that are derived of interpreted Petri nets, which has been proven as an efficient tool for modeling, analysis and control of DES. In this context, systems are modeled in different levels of abstraction: a conceptual model which is obtained by using the PFS (Production Flow Schema) technique level, and a functional model by using MFG (Mark Flow Graph) and its extensions. The MFG abstraction level describes details in a functional form, where are preserved the description activities of previous levels. The methodology proposal confirmed to be useful and efficient to elevator systems modeling, when allowing the functional specification of the whole system (object of control and control system), and strategies that facilitate its integration with others building systems.

Ao longo das últimas décadas, o paradigma de sistemas críticos em segurança vem sofrendo transformações como forma de se adequar às novas necessidades demandadas, tais como redução de custos e aumento da produtividade. No Sistema de Gerenciamento de Tráfego Aéreo, esta transformação é preconizada pelo paradigma CNS/ATM (Communication, Navigation, Surveillance / Air Traffic Management), baseado no uso de novas tecnologias digitais, sobretudo satélites, aplicadas à comunicação, à vigilância, à navegação e ao gerenciamento do tráfego aéreo. O CNS/ATM visa reduzir as restrições do atual paradigma de tráfego aéreo como forma de atender sua crescente demanda, mantendo (ou melhorando) os atuais níveis de segurança. Porém, esta mudança de paradigma traz consigo novos desafios e necessidades, sobretudo, quanto à forma de se avaliar os sistemas resultantes. Em face destes novos desafios e problemas enfrentados, este trabalho propôs um método de avaliação de risco, constituído pela união dos métodos \"absoluto\" e \"relativo\" preconizados pela Organização da Aviação Civil Internacional (OACI), pelo emprego do formalismo das redes de Petri Fluidas e Estocásticas (RPFE) na modelagem dos sistemas, e pela comparação entre os valores de métricas de segurança estimados para o sistema avaliado e para um sistema legado. Este método foi aplicado para avaliar a segurança na mudança do atual paradigma de vigilância aérea, baseado em equipamentos Radar, para o paradigma de Vigilância Dependente Automática por Radiodifusão (ADS-B). Como conclusões, o método proposto mostrou-se promissor para avaliar a segurança de sistemas baseados nos atuais paradigmas de sistema críticos em segurança, especialmente o CNS/ATM, onde o formalismo das RPFE proporcionou modelar suas principais características, e a simulação por eventos discretos permitiu estimar as métricas desejadas. Além disso, a ADS-B mostrou-se uma aplicação viável para a vigilância no Sistema de Controle de Tráfego Aéreo, sendo capaz de reduzir o nível de exposição das aeronaves a eventos de perda de separação e, assim, melhorar os níveis de segurança do tráfego aéreo. / In last decades, the safety critical systems paradigm has changing to adapt itself to new necessities, such as costs reduction and productivity demand growth. In the Air Traffic System, those changes are ruled by CNS/ATM paradigm (Communication, Navigation, Surveillance / Air Traffic Management), based on new digital Technologies, mainly Satellites, applied to Communication, Surveillance, Navigation and Air Traffic Management. CNS/ATM intends to reduce the restrictions of current air traffic paradigm, enabling the growth of air traffic capacity without affecting current safety levels. However, this new paradigm brings together new challenges and needs, mainly related to safety assessment. In face of these new challenges, this work proposed a method of risk assessment constituted by the union of the \"absolute\" and \"relative\" assessment methods adopted by the International Civil Aviation Organization (ICAO), by modeling systems using Fluid Stochastic Petri Nets (FSPN) formalism, and by comparison between safety metrics obtained from proposed and legacy system simulations. This method was applied to assess a new concept of air traffic surveillance, named \"Automatic Dependent Surveillance - Broadcasting\" (ADS-B). As main conclusions, the proposed method was promising to assess system safety properties based on current safety critical system paradigm, especially the CNS/ATM, where FSPN formalism provided important modeling capabilities and discrete event simulation allowed estimating the desired safety metric. Besides, ADS-B has meaningfully reduced the separation losses risks and, therefore, it could be used to air traffic control surveillance system to improve capacity and/or safety levels of air traffic system.

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.

O sistema de elevadores como equipamento para o transporte vertical de pessoas e bens é um componente fundamental no projeto de edifícios e, neste âmbito, a disponibilidade e eficiência do seu serviço deve ser objeto de cuidadosa análise em função de sua influência no desempenho e produtividade das atividades dos usuários do prédio. Neste contexto e considerando especificamente os edifícios inteligentes cuja finalidade é a otimização a nível estrutural e funcional do edifício como um todo, e onde a integração entre seus sistemas cumpre um papel fundamental para atingir estes objetivos, o presente trabalho propõe uma metodologia para a modelagem de sistemas de elevadores nestes prédios, que considera a sua integração com outros sistemas prediais. A abordagem empregada no desenvolvimento deste trabalho baseia-se na caracterização dos sistemas de elevadores como sistemas a eventos discretos (SED), pois sua dinâmica é definida através da ocorrência de eventos e a manutenção de estados discretos. Assim, na metodologia utiliza-se técnicas derivadas das redes de Petri (redes de Petri interpretadas), de comprovada eficiência para a modelagem, análise e controle de SEDs. Estas ferramentas são usadas através de uma abordagem estrutural, onde o sistema é modelado em diferentes níveis de abstração: um modelo conceitual obtido pelo uso da técnica PFS (Production Flow Schema) em um primeiro nível, e o refinamento deste para modelos funcionais através do uso do MFG (Mark Flow Graph) e suas extensões, onde são preservadas as estruturas das atividades do nível superior e são descritos os detalhes em um nível funcional. A metodologia proposta confirmou ser útil e eficiente para a modelagem do sistema de elevadores em edifícios inteligentes, ao permitir a especificação do modelo funcional de todo o sistema (objeto de controle e sistema de controle) e das estratégias que facilitam a sua integração com outros sistemas prediais / The elevator system as mean for the vertical transport of people and goods is a fundamental component in the design of buildings. The availability and efficiency of this service must be object of careful analysis due to its influence on the performance and productivity of the building users' activities. In intelligent buildings, the purpose is the optimization of its structural and functional levels and where also the integration between all building systems accomplishes a fundamental role to reach these objectives. In this context, this work proposes a methodology for the modeling of elevator systems in these buildings, which consider your integration with others buildings systems. The approach developed in this work is based on the characterization of elevator systems as Discrete Event Systems (DES), since the dynamic behavior is defined through the discrete events and discrete states. The proposed methodology uses techniques, that are derived of interpreted Petri nets, which has been proven as an efficient tool for modeling, analysis and control of DES. In this context, systems are modeled in different levels of abstraction: a conceptual model which is obtained by using the PFS (Production Flow Schema) technique level, and a functional model by using MFG (Mark Flow Graph) and its extensions. The MFG abstraction level describes details in a functional form, where are preserved the description activities of previous levels. The methodology proposal confirmed to be useful and efficient to elevator systems modeling, when allowing the functional specification of the whole system (object of control and control system), and strategies that facilitate its integration with others building systems.

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.

A methodology for representing and analyzing manufacturing systems in a hybrid systems framework for control reconfiguration purposes in the presence of defects and failures at the product and system levels is presented. At the top level, a supervisory Petri net directs parts/jobs through the manufacturing system. An object-based hybrid systems model that incorporates both Petri nets at the event-driven level and differential equations at the time-driven level describes the subsystems. Rerouting capabilities utilizing this model at the product and operation levels were explained. Simulations were performed on a testbed model for optimal time and mode transition cost to determine the route for parts. The product level reconfiguration architecture utilizes an adaptive network-based fuzzy inference system (ANFIS) to map histogram comparison metrics to set-point adjustments when product defects were detected. Tests were performed on good and defective plastic parts from a plastic injection molding machine. In addition, a mode identification architecture was described that incorporates both time- and event-driven information to determine the operating mode of a system from measured sensor signals. Simulated data representing the measured process signals from a Navy ship chiller system were used to verify that the appropriate operating modes were detected.

L'objectif de cette thèse est de contribuer à l'élaboration de méthodes d'aide à la conception de systèmes coopératifs en prenant en compte les contraintes temporelles de manière quantitative. L'approche développée est fondée sur les réseaux de Petri, la logique linéaire et les graphes de contraintes temporelles. C'est une approche orientée « événements » et non orientée « états » comme c'est souvent le cas dans les approches fondées sur les réseaux de Petri. Elle est décomposée en deux étapes : une étape d'analyse « qualitative » et une étape d'analyse « quantitative ». La première consiste à obtenir les relations de causalité entre les événements appartenant à un scénario donné. L'équivalence entre un arbre de preuve en logique linéaire et le processus fini obtenu par dépliage d'un réseau de Petri à partir du même marquage initial montre que ces relations sont des relations de précédence. L'introduction de la notion de séquent caractéristique permet de mettre en Suvre une approche compositionnelle des processus à partir des règles du calcul des séquents. La deuxième étape consiste à passer du graphe décrivant les relations de précédence à un graphe de contraintes temporelles exprimant de façon linéaire l'ensemble des contraintes temporelles quantitatives que doivent vérifier les dates des franchissements des transitions dans un scénario. Il devient ainsi possible d'exploiter tous les résultats des techniques classiques d'analyse et de propagation de contraintes. Cette démarche est complètement cohérente avec les réseaux de Petri p-temporels mais difficilement compatible avec les t-temporels car ils engendrent des ensembles de contraintes qui sont plus complexes. Nous avons illustré cette démarche par un problème simple d'ordonnancement de documents multimédias. Nous avons par la suite montré comment, pour les réseaux de Petri t-temporels, nous pouvions calculer les dates de franchissements et les durées de séjour des jetons dans les places en restant sous une fo rme symbolique dans le cadre de la sémantique faible.