La Baie de Marennes Oléron, première zone Européenne d’ostréiculture, est exposée aux apports de contaminants métalliques provenant de la Charente et la Seudre, dont les apports en eau et particules se font directement dans la baie, mais également par la Gironde dont les apports sont indirects et tributaires des forçages hydrologiques et météorologiques. Un réseau de surveillance (2006-2007) a été mis en place sur le fleuve Charente et sur la Seudre afin de déterminer leurs flux bruts métalliques dissous (<0,2µm) et particulaires. En raison d’un faible débit moyen annuel, les flux métalliques de la Seudre sont négligeables. En Charente, les concentrations dissoutes et particulaires en Cd et Cu sont semblables ou supérieurs à celles de la Garonne, représentant des flux spécifiques supérieurs à ceux de la Garonne. La réactivité des ETM dans les estuaires de la Gironde et de la Charente, dans la zone littorale et dans la Baie de Marennes Oléron a été documentée à partir d’une vingtaine de campagnes océanographiques et d’un suivi mensuel (2007) sur la partie sud de la Baie de Marennes Oléron. En Gironde, les concentrations dissoutes totales en Cd, V et U le long des gradients turbides et salins sont représentées essentiellement (>90%) par la fraction labile. En revanche, 30-70% de Co dissous et 50-60% de Cu dissous sont fortement complexés. Les 15 campagnes sur l’estuaire de la Gironde en conditions hydrologiques et saisonnières très contrastées ont permis de documenter la distribution et la spéciation des ETM et de proposer un modèle de calcul des flux nets annuels dissous des ETM exportés en zone littorale. En couplant des mesures ADCP à des prélèvements géochimiques à l’embouchure de la Gironde pendant un cycle tidal et pour différentes conditions hydrologiques, nous avons déterminé les flux résiduels en ETM particulaires au cours d’un cycle tidal. La mise en relation de ces résultats avec un modèle hydro-sédimentaire a permis d’estimer les flux nets en ETM particulaires de la Gironde pour l’année 2007. Pour tracer le transfert des particules de la Gironde dans la Baie de Marennes Oléron nous avons utilisé les rapports élémentaires de la fraction résiduelle des particules et analysé le panache turbide de la Gironde par imagerie satellite. Ces deux approches indépendantes suggèrent que 50% à 75% de la masse totale de MES véhiculées annuellement dans la baie proviennent de la Gironde et transitent majoritairement par le Pertuis de Maumusson. Les résultats inédits obtenus à partir des mesures in situ et d’expérimentations de désorption ont permis de proposer un bilan annuel des flux métalliques des différentes formes de Cd et Cu intégrant la Baie de Marennes Oléron. Près de 61% des apports totaux en Cd dans la Baie de Marennes Oléron sont issus des apports dissous de la Charente alors que 60% des apports totaux en Cu sont représentés par le transfert de particules de la Gironde. / The Marennes-Oléron Bay, Europe’s major oyster production zone, receives direct particle and water inputs by the Charente and the Seudre Rivers. The bay is also indirectly influenced by inputs from the Gironde Estuary, depending on hydrological and meteorological forcing. Fluvial trace metal inputs via the Charente and Seudre Rivers were evaluated during 2006-2007. Trace metal fluxes in the Seudre River were negligible due to its low mean annual freshwater discharge. Dissolved (<0.2µm) and particulate Cd and Cu concentrations and specific fluxes in the Charente River were similar or higher than those in the Garonne River. The reactivity of trace metals in the Gironde/Charente Estuaries, in the coastal zone and in the Marennes-Oléron Bay was investigated by 20 oceanographic campaigns and by a monthly monitoring (2007) of the Southern Marennes-Oléron Bay. The major parts (>90%) of total dissolved Cd, V and U concentrations along the turbidity and the salinity gradients were present in the labile fraction. In contrast, 30-70% of dissolved Co concentrations and 50-60% of dissolved Cu were strongly-bound to dissolved complexes. Based on 15 dissolved trace metal profiles, we evaluated the variability of dissolved trace metal distributions and speciation in the Gironde Estuary and proposed an empirical model for the estimation of dissolved trace metal annual net fluxes exported to the coastal ocean. Coupling ADCP measurements with geochemical data obtained at the Gironde Estuary mouth during entire tidal cycles and for contrasting conditions, we determined the residual particulate trace metal daily net fluxes. Comparison of our results with a hydro-sedimentary model allowed estimating the particulate trace metal net fluxes of the Gironde Estuary at the annual scale for 2007. Characteristic trace metal ratios in the residual particulate fraction of SPM and sediment were identified to trace particle transfer from the Gironde to the Marennes-Oléron Bay. This approach and the study of the shape of the turbid plume by satellite imaging suggest that the Gironde Estuary contributes 50-75% of the total annual SPM inputs into the bay via the Maumusson inlet. Based on these original results and combining in situ measurements and desorption experiments we proposed an annual budget of Cd and Cu fluxes into the Marennes-Oléron Bay. Dissolved Cd fluxes of the Charente Estuary accounted for ~61% of the total Cd inputs into the Marennes Oléron Bay, while ~60% of the total Cu inputs were transported by the particles from the Gironde Estuary.

Le problème de représentation automatique de la signification logique des énoncés ambigus en langage naturel a suscité l'intérêt des chercheurs dans le domaine de la sémantique computationnelle et de la logique. L'ambiguïté dans le langage naturel peut se manifester au niveau lexical / syntaxique / sémantique de la construction de sens, ou elle peut être causée par d'autres facteurs tels que la grammaticalité et le manque de contexte dans lequel la phrase est effectivement prononcée. L'approche traditionnelle Montagovienne ainsi que ses extensions modernes ont tenté de capturer ce phénomène en fournissant quelques modèles qui permettent la génération automatique de formules logiques. Cependant, il existe un axe de recherche qui n'est pas encore profondément étudié: classer les interprétations d'énoncés ambigus en fonction des préférences réelles des utilisateurs de la langue. Ce manque suggère une nouvelle direction d'étude qui est partiellement explorée dans ce mémoire en modélisant des préférences de sens en alignement avec certaines des théories de performance préférentielles humaines bien étudiées disponibles dans la littérature linguistique et psycholinguistique.Afin d'atteindre cet objectif, nous suggérons d'utiliser / d'étendre les Grammaires catégorielles pour notre analyse syntaxique et les Réseaux catégoriels de preuve comme notre analyse syntaxique. Nous utilisons également le Lexique Génératif Montagovien pour dériver une formule logique multi-triée comme notre représentation de signification sémantique. Cela ouvrirait la voie à nos contributions à cinq volets, à savoir, (i) le classement de la portée du quantificateur multiple au moyen de l'opérateur epsilon de Hilbert sous-spécifié et des réseaux de preuve catégoriels; (ii) modéliser la gradation sémantique dans les phrases qui ont des coercitions implicites dans leurs significations. Nous utilisons un cadre appelé Montagovian Generative Lexicon. Notre tâche est d'introduire une procédure pour incorporer des types et des coercitions en utilisant des données lexicales produites par externalisation ouverte qui sont recueillies par un jeu sérieux appelé JeuxDeMots; (iii) l'introduction de nouvelles métriques sensibles au référent basées sur la localité pour mesurer la complexité linguistique au moyen de réseaux de preuve catégoriels; (iv) l'introduction d'algorithmes pour l'achèvement des phrases avec différentes mesures linguistiquement motivées pour sélectionner les meilleurs candidats; (v)l'intégration de différentes métriques de calcul pour les préférences de classement afin de faire d'elles un modèle unique. / The problem of automatic logical meaning representation for ambiguous natural language utterances has been the subject of interest among the researchers in the domain of computational and logical semantics. Ambiguity in natural language may be caused in lexical/syntactical/semantical level of the meaning construction or it may be caused by other factors such as ungrammaticality and lack of the context in which the sentence is actually uttered. The traditional Montagovian framework and the family of its modern extensions have tried to capture this phenomenon by providing some models that enable the automatic generation of logical formulas as the meaning representation. However, there is a line of research which is not profoundly investigated yet: to rank the interpretations of ambiguous utterances based on the real preferences of the language users. This gap suggests a new direction for study which is partially carried out in this dissertation by modeling meaning preferences in alignment with some of the well-studied human preferential performance theories available in the linguistics and psycholinguistics literature.In order to fulfill this goal, we suggest to use/extend Categorial Grammars for our syntactical analysis and Categorial Proof Nets as our syntactic parse. We also use Montagovian Generative Lexicon for deriving multi-sorted logical formula as our semantical meaning representation. This would pave the way for our five-folded contributions, namely, (i) ranking the multiple-quantifier scoping by means of underspecified Hilbert's epsilon operator and categorial proof nets; (ii) modeling the semantic gradience in sentences that have implicit coercions in their meanings. We use a framework called Montagovian Generative Lexicon. Our task is introducing a procedure for incorporating types and coercions using crowd-sourced lexical data that is gathered by a serious game called JeuxDeMots; (iii) introducing a new locality-based referent-sensitive metrics for measuring linguistic complexity by means of Categorial Proof Nets; (iv) introducing algorithms for sentence completions with different linguistically motivated metrics to select the best candidates; (v) and finally integration of different computational metrics for ranking preferences in order to make them a unique model.

This study examines the Swedish Stock Exchange during the time period of 1998-2016. Where the purpose is to investigate and compare five different investment strategies to see if these investment strategies can create excess return on their investments, after adjustment for risk. The investment strategies can be found on the internet, and be used after purchasing a smaller amount of money, therefore the results can be applied to all investors independent on their level of experience. The results for the different investment strategies are not clear, the different tests give mixed results which leaves four of five hypotheses unanswered. However, there is one strategy that can be rejected, it cannot beat the market, which is the Net-Nets strategy. In general, one could thus say that the investment strategies can create higher return compared to the market, but that these returns are random. Therefore, it requires a longer time period for the investor as well as higher risk, since one never knows when this large return will be given.

Apresenta uma análise da estimação de custos em sistemas de manufatura utilizando rede de Petri (PN), ferramenta gráfica e matemática para modelagem e simulação. Esta análise permite a apresentação de um sistema aplicável à programação e otimização de processos de fabricação aliadas à estimação dos custos ao longo do processo. Para uma determinada peça, a partir de conceitos sobre custeio de produtos, é proposto um modelo que visa conectar as transições da PN com as informações de custos de produção. O estudo de caso mostra que informações importantes à tomada de decisão podem ser obtidas através do uso de uma metodologia que incorpore planejamento de processos, métodos de custeio e redes de Petri. Finalmente, traz sugestão de um trabalho subseqüente: a partir do modelo proposto, implementar um template no editor/simulador de redes de Petri, Petri Net Tools 2000, capaz de realizar os cálculos necessários para estimativas de custo e fornecer resultados relevantes para um planejamento real. / This work presents a cost estimation analysis in manufacturing systems based in Petri net (PN), which is a graphical and mathematical tool. This analysis allows the presentation of a system, applicable to the programming and optimizing of manufacturing processes joined with cost estimation. A cost model is proposed using concepts of product costing. It seeks for connecting PN transitions to the data manufacturing cost of a certain part. The case study shows that important information to decision support can be found through the use of a methodology which joins process planning, costing systems and Petri nets. There is also a suggestion of a later work: a template implementation, on Petri Net Tools 2000 editor/simulator of PN models, which is able to accomplish the necessary calculations for cost estimates and, to supply important results to a real planning.

Os sistemas de manufatura há muito vêm sendo objeto de interesse por profissionais e pesquisadores devido à busca de melhores técnicas visando o aumento da produtividade bem como pelo aumento da competitividade empresarial ao longo dos anos. Dentre seus componentes, o sistema de movimentação de materiais merece atenção especial pois, apesar de não aumentar o valor do produto, é responsável por manter o fluxo de materiais entre máquinas, células de manufatura, centros de custos ou mesmo entre empresas, que é imprescindível para qualquer sistema produtivo. Neste contexto, o presente trabalho propõe uma metodologia para a modelagem de sistemas flexíveis de movimentação de materiais e partes em ambiente fabril, focando-se em sistemas cuja movimentação possa ser realizada por VATs (Veículos Autônomos de Transporte). Considerando-se o sistema de movimentação de materiais como sendo um sistema a eventos discretos (SEDs), pode-se empregar técnicas derivadas das Redes de Petri como o PFS (Production Flow Schema) e o E-MFG (Enhanced Mark Flow Graph) na modelagem de tais sistemas. Para tanto, foram introduzidos conceitos de orientação a objetos ao E-MFG de forma a ampliar sua capacidade de modelagem, possibilitando a migração de um paradigma de modelagem orientada a processos para um de modelagem híbrida orientada a processos e a objetos. Como estudo de caso, apresenta-se a modelagem de uma simplificação do sistema de movimentação de materiais da Mercedes Benz do Brasil, situada em São Bernardo do Campo, São Paulo, para a qual se aplica a metodologia proposta. / Manufacturing systems have been object of interest of many professionals and researchers through the years due to the search of better methods for raising goods productivity and managerial competitiveness. Among its components, the material movement system deserves special attention because even not increasing the product value, it is responsible for keeping the flow of materials between machines, manufacturing cells, cost centers and also between companies, which is indispensable for any productive system. In this context, this work proposes a methodology for modeling flexible systems for materials and parts movement in the industrial environment, focusing on systems whose movement can be performed by AGVs (Autonomous Guided Vehicles). Considering the materials movement system as a Discrete Event System (DES), techniques derived from Petri Nets as PFS (Production Flow Schema) and E-MFG (Enhanced Mark Flow Graph) can be used for modeling those systems. To this purpose, concepts of object orientation are introduced to E-MFG in order to increase its modeling capacity, allowing the migration from the process oriented modeling paradigm to an hybrid object and process oriented modeling. A simplification of the materials movement system of the plant of "Mercedes Benz do Brasil", which is located in São Bernado do Campo, São Paulo, was used as a study case to illustrate the methodology presented.

A arquitetura IP Multimedia Subsystem, proposta pelo consórcio 3rd Generation Partnership Project como base para o suporte à convergência entre telefonia móvel e a Internet, define uma série de elementos arquiteturais, entre os quais, o componente Call Session Control Function e o protocolo Session Initiation Protocol. Session Initiation Protocol é um protocolo da camada de aplicação utilizado para estabelecer, modificar e terminar sessões multimídia entre dispositivos. Em redes baseadas na arquitetura IP Multimedia Subsystem, o Session Initiation Protocol é o responsável pela comunicação entre dispositivos e a rede, e entre os componentes responsáveis pelo gerenciamento de sessão. Nos últimos anos, estudos detectaram degradação de desempenho em redes baseadas na arquitetura IP Multimedia Subsystem em função das características centralizadas do Session Initiation Protocol e dos componentes de gerenciamento de sessão. Este trabalho apresenta uma arquitetura distribuída para redes baseadas em IP Multimedia Subsystem, tendo como fundamento o paradigma de computação paralela baseado em espaço de tuplas onde os servidores são organizados em uma rede P2P, com objetivo de prover uma infraestrutura escalável e tolerante a falhas. A validação da arquitetura em termos de desempenho e escalabilidade se deu através de modelagem formal e simulação com Redes de Petri Coloridas. / The IP Multimedia Subsystem architecture, proposed by the 3rd Generation Partnership Project consortium as basis to support the convergence between mobile networks and the Internet, defines a set of architectural elements, among them, the Call Session Control Function and the Session Initiation Protocol. The Session Initiation Protocol is an application layer protocol used to establish, modify and terminate sessions between devices. On the IP multimedia subsystem based network, the Session Initiation Protocol play a key role on the communication between devices and the network, and between session management components. In the last years, studies have detected a performance bottleneck on IP multimedia subsystem networks due to centralized characteristic of the Session Initiation Protocol and in Session Control components. This work shows a distributed architecture for IP Multimedia Subsystem networks based on the tuple space paradigm, and the servers structured in a P2P network, aiming to achieve a scalable and fault-tolerant infrastructure. The validation of the architecture on the performance and scalability took place through the Coloured Petri Net formal modeling and simulation.

O comércio de retalhos e resíduos têxteis está localizado nas ruas do Brás, antigo bairro industrial e operário da cidade de São Paulo. Esse bairro, hoje, concentra um grande número de indústrias e lojas de confecções, que vendem no atacado e no varejo para \"sacoleiras\" de todas as partes do Brasil. O comércio de retalhos vai nascer nos interstícios das antigas indústrias têxteis e, posteriormente, se alimentar do rejeito da indústria da confecção que fornece, diariamente, toneladas de resíduos e retalhos para serem comercializados pelos \"retalheiros\". Uma parte desses retalhos e rejeitos é comprada por costureiras da Grande São Paulo e até mesmo por \"sacoleiras\", sendo que a maior parte dessa mercadoria é enviada para Santa Cruz do Capibaribe - cidade do interior pernambucano, que constitui em pólo de confecções de \"sulanca\". São vestuários de qualidade considerada inferior, consumidos, predominantemente, por uma população de baixa renda. O nordestino de menor poder aquisitivo passa a ser consumidor do rejeito das confecções do Centro Sul. O comércio de retalhos e resíduos é controlado, predominantemente, por migrantes nordestinos, formando uma rede de pessoas e mercadorias em torno dessa atividade. Desta forma, procuramos estudar como tais migrantes foram mobilizados para trabalhar nesse comércio nas ruas do Brás. Estudamos as transformações do bairro, desde a ocupação dos italianos até a chegada dos nordestinos, no sentido de entender a presença do comércio em suas ruas. Ao identificar as conexões que esse espaço mantém com outros espaços, construindo uma malha de homens e mercadorias, optamos por seguir a circulação da mercadoria - retalho até o seu destino final, qual seja, as feiras da sulanca de Pernambuco. Dentre as múltiplas problematizações que a pesquisa traz à tona, destacamos as redes sociais como um instrumento mobilizador do migrante comerciante autônomo de retalhos contribuindo para a ampliação do capital / Trading cloth patches and textile remainders is carried out in the streets of the Brás neighborhood, an industrial and working class old district in São Paulo. It now concentrates several industries as well as wholesale and retail clothing stores meant for \"sacoleiras\" coming from all over Brazil. The patch trade originates in the interstices of old textile industries. Later it feeds on refuses of clothing industries that daily supply tons of remainders and patches to be traded by the \"retalheiros\". These patches and refuses are partly bought both by sewing women in greater São Paulo and by \"sacoleiras\". Most goods are sent to Santa Cruz do Capibaribe, in the hinterlands of Pernambuco State, which is a \"sulanca\" manufacturing pole. It merely consists of poorer quality clothing, mostly consumed by a lower income population. The lower income northeastern citizen becomes a buyer of fabric refuses from the Southern Center. The patch and remainder trade is mostly controlled by northeastern migrants, who form a net of people and merchandise based on this activity. Hence, this dissertation aimed at studying how these migrants were mobilized to work in this trade in the streets of Brás. In order to understand this process, the work also investigated the changes undergone by the district, from the Italian to the northeastern Brazilian occupation on the area. Once the connection among this and other areas was identified by the people/goods net evolution the patch-goods circulation was followed to one of its ends, namely the \"sulanca\" fairs in Pernambuco. Among the manifold questions raised by this research, attention should be drawn to the social nets as a mobilizing means of the free-lance migrant, who trades patches that contributes to capital increase

As centrais de carga são um importante mecanismo de coordenação do mercado de fretes, tendo como um de seus objetivos ampliar as informações sobre este mercado, reduzindo a incerteza na obtenção de cargas e os custos de transportes. Com o avanço da internet, a possibilidade de criação de centrais de cargas abrangendo grandes áreas e um grande número de usuários tornou-se uma alternativa atraente, utilizada cada vez com maior freqüência. Entretanto, pouco se conhece sobre a sua utilização em atividades ligadas à área de logística. Assim, este trabalho objetivou caracterizar as centrais de cargas na internet, a sua utilização, por embarcadores e transportadoras, em atividades logísticas e testar a hipótese de que diferentes empresas, trabalhando com diferentes tipos de produtos, terão percepções e necessidades diferentes em relação aos serviços oferecidos. As análises fatorial e de conglomerados foram utilizadas para se atingir esses objetivos. No período estudado observou-se um aumento significativo no número de serviços disponíveis em diversos países e que as empresas possuem uma série de características comuns, como a orientação voltada tanto para embarcadores como transportadores, a formação de preços por meio de leilões e o aumento no número de centrais com participação na transação efetuada por seus usuários. O grupo de empresas estudadas caracterizou-se por transportar/produzir cargas gerais e produtos agrícolas, empregando a internet principalmente nas áreas administrativas, para a contratação de fretes e tomadas de preço. Os serviços oferecidos atualmente pelas centrais foram considerados importantes pelas empresas pesquisadas, que ressaltaram a necessidade de conhecer e identificar os parceiros com que se negocia na rede. A análise fatorial permitiu agrupar as características e serviços que aparecem com mais freqüências nos sites, gerando 6 fatores identificados como: serviços prestados, segurança e tamanho da comunidade de usuários, serviços adicionais, pré-seleção de participantes e abrangência dos serviços, integração e forma de negociação e imparcialidade do site. Esses fatores indicam quais os pontos que devem ser considerados para o estabelecimento de novos sistemas ou na melhoria dos existentes. Na análise de conglomerados foram obtidos 3 grupos de empresas. O grupo 1 apresentou um número equivalente de embarcadores e transportadores, que trabalham principalmente com cargas gerais e agrícolas, estando dividido entre empresas que utilizam, ou não, a internet. Esse grupo apresenta a melhor distinção entre a importância atribuída aos serviços, quando comparado aos outros dois. O conglomerado 2 possui principalmente operadores logísticos e transportadoras, que trabalham com a maior variedade de cargas entre os grupos. No grupo predominam as empresas que não utilizam a internet. Esse conglomerado atribuiu os maiores valores às questões referentes aos serviços oferecidos pelas centrais, considerando-as como importantes. O c onglomerado 3 é formado principalmente por embarcadores, possui o maior número de usuários da internet e atribuiu os menores valores aos serviços avaliados. Com base nesses resultados, pode-se inferir que empresas diferentes, no caso embarcadores e transportadores, atribuem importância diferente aos serviços oferecidos pelas centrais de cargas. Deve -se considerar que os resultados encontrados são válidos apenas para as empresas pesquisadas e focam a realidade de um período determinado, exigindo um acompanhamento de seu desenvolvimento ao longo do tempo. / Load matching services are a ve ry important mechanism for coordination of the freight market and enlarging the information on such market is one of their targets, in order to reduce the uncertainty in the load obtainment and transportation costs. With the advance of the internet, the possibility of creation of load matching services including large areas and a large number of users became an attractive alternative, which is used in larger frequency. Nevertheless its application related to activities in the Logistics is not well known yet. This study aims at the characterization of load matching services in the internet, its use by shippers and carriers in Logistic activities and also the test of the hypothesis that different types of companies dealing with different types of products will have different perceptions and needs on the available services. The factor analyses and cluster analyses were used in order to reach such objectives. During the period the study was conducted it has been observed a significant increase in the number of services available in several countries and that the companies have a series of common characteristics, such as the orientation either to shippers as well as tocarriers; price formation by means of auction and the increase of the load matching services with participation of their users in the transaction. Transporting/producing general cargoes and agricultural products using the internet mainly in the administrative areas for hiring the freights and price checkouts have characterized the group of companies that was studied. The current services offered by the load matching services were considered important by the companies that were surveyed; such companies highlighted the need of knowing and identifying the partners with whom they deal in the web. The factor analyses allowed to group up the characteristics and services that are more common in the sites, generating 6 factors identified as services offered, safety and size of the user's community, additional services, pre-selection of participants and wide ranging of services, integration and negotiation style and impartiality on the site. These factors indicate which aspects must be taken into account in order to establish new systems or to improve the existing ones. In the cluster analyses, three different groups were identified. Group 1 presented an equivalent number of shippers and carriers that deal mainly with general and agricultural cargoes and that are split into companies that use or not the internet. This group shows the best distinction between the importance given to the services when compared with the other groups. Group 2 has mainly logistic operators and carriers that work with the biggest variety of loads among the groups. In this group there is a predominance of companies that do not use the i nternet. This group has attributed the biggest values to aspects referring to the services offered by the load matching services, considering them as very important. Group 3 is made up mainly by shippers, has the largest number of the internet users and has the least values to the evaluated services. Based on these results, one can infer that different companies (in the case shippers and carriers) give different importance to the services offered by the load matching services. One must have in mind that the results obtained are valid only to the companies that were studied and that the research focuses the day-to-day reality of a specific period of time what, in turn, creates the need of its posterior development in time.

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.

In dieser Arbeit geht es um die schrittweise Verfeinerung verteilter Algorithmen. Dabei wird ein einfacher Algorithmus, der einige gewünschte Eigenschaften hat, Schritt für Schritt zu einem komplexen Algorithmus verfeinert, der konkrete Implementationsanforderungen erfüllt, so daß in jedem Schritt die gewünschten Eigenschaften erhalten bleiben. Wir stellen einen neuen eigenschaftserhaltenden Verfeinerungsbegriff vor, der auf der kausalen Ordnung der Aktionen eines Algorithmus basiert. Diesen Begriff definieren wir als Transitionsverfeinerung für elementare Petrinetze und diskutieren Beweiskriterien. Danach definieren und diskutieren wir die simultane Verfeinerung mehrerer Transitionen. Zur Modellierung komplexer verteilter Algorithmen sind elementare Petrinetze oft nicht adäquat. Wir benutzen deshalb algebraische Petrinetze. Wir definieren Transitionsverfeinerung für algebraische Petrinetze und stellen einen Zusammenhang zur simultanen Verfeinerung von Transitionen in elementaren Petrinetzen her. Transitionsverfeinerung ist besonders für Verfeinerungsschritte geeignet, in denen synchrone Kommunikation zwischen Agenten durch asynchronen Nachrichtenaustausch ersetzt wird. Wir zeigen dies am Beispiel eines komplexen verteilten Algorithmus, zur Berechnung des minimalen spannenden Baumes in einem gewichteten Graphen. Wir zeigen die Korrektheit dieses Algorithmus in mehreren Schritten, von denen einige Schritte Transitionsverfeinerungen sind. In anderen Schritten sind klassische Verfeinerungsbegriffe ausreichend. Wir übertragen deshalb auch einen klassischen Verfeinerungsbegriff in unser formales Modell. / The topic of this PhD thesis is the stepwise refinement of distributed algorithms. Stepwise refinement starts with a simple algorithm with certain desired properties. This algorithm is refined step by step such that the desired properties are preserved in each refinement step. The result is a complex distributed algorithm which satisfies concrete implementation requirements and which still has the desired properties. We propose a new property preserving notion of refinement which is based on the causal ordering of actions of an algorithm. We call this notion transition refinement and we define it first for elementary Petri nets. Furthermore, we discuss proof criteria. Then, we define and discuss the simultaneous refinement of several transitions. For modelling complex distributed algorithms, we use algebraic Petri nets instead of elementary Petri nets. We define transition refinement for algebraic Petri nets, and we show its relationship to simultaneous transition refinement in elementary Petri nets. Transition refinement is particularly suitable for refinement steps in which synchronous communication between agents is replaced by asynchronous message passing. We show this by means of a complex distributed algorithm for determining the minimal spanning tree of a weighted graph. We prove the correctness of this algorithm in several steps. Some of these steps are transition refinements. For other steps, well-known notions of refinement are sufficient. Therefore, we also carry over a well-known notion of refinement into our formal model.