O objetivo dessa tese é formalizar a análise das redes de Petri temporais usando a álgebra intervalar como ferramental matemático. A álgebra intervalar é tradicionalmente usada na solução de problemas relacionados com imprecisão. Por sua vez, as redes de Petri temporais se caracterizam, por definição, por possuir um intervalo temporal que delimita os períodos mínimos e máximos de sensibilização das transições. Em consequência, a imprecisão quanto a data de disparo das transições ´e denotada por um intervalo. Assim, neste trabalho, a dinâmica dos intervalos de disparos ao longo da evolução da rede é modelada por uma equação linear intervalar, que possibilita o cálculo de intervalos de tempo de ocorrências de transições sem que seja necessário explorar, completa ou parcialmente, o espaço de estados. Essa mesma equação pode ser usada para tratar do problema inverso: identificar sequências de disparos de transições que permitam alcançar uma determinada marcação respeitando uma janela temporal pré-definida. Este problema foi denominado de alcançabilidade temporal. Ao longo do desenvolvimento dessa abordagem, outros importantes resultados foram obtidos, tais como: método enumerativo usando tempo global para análise via alcançabilidade da rede, métodos de redução baseados em aproximações intervalares, redução do espaço de estados, e uma alternativa para construção do grafo de estados com domínios relativos e intervalos de disparos com tempo absoluto. A abordagem desenvolvida foi aplicada a diferentes problemas a fim de calcular grandezas como: tempos máximo e mínimo entre a ocorrência de duas transições, validação de sequências de disparos, tempos de ciclos, entre outras. / The objective of this thesis is to establish formal conditions for time Petri nets analysis by interval algebra. The interval algebra is traditionally used as a mathematical tool in the solution of problems related to uncertainty. In fact time Petri nets are characterized by presenting an uncertainty at the moment of its transitions firing. This imprecision is denoted by a firing interval. Thus, in this work the dynamics of the firing intervals throughout the evolution of the net is represented by a linear interval equation, which makes possible the calculation of transition firing intervals without generating the whole space of states to be explored, completely or partially. Also, this interval equation is used to solve a kind of inverse problem to the previous one. That is, given a time specification for a time Petri net to evalue from a state to another one any to compute the possibilities of firings between these two states, in case that it exists. Throughout the development of the approach, other important results have been obtained, such as: reduction methods for time Petri nets baseds interval approximation, reduction of the state space, and an alternative for the construction of the state graph with relative and absolute times. The developed approach was applied to different problems to compute metrics such as: maximum and minimum time separation ocurrence of two transition, the scheduling validation of firing sequence, times of cycles, among others.

Les réseaux de Chebyshev sont des systèmes de coordonnées sur les surfaces que l'on obtient par cisaillement d'un domaine du plan. Ceux-ci sont utilisés en particulier pour modéliser les gridshells qui constituent une construction architecturale notamment reconnue pour son faible coût environnemental. La difficulté principale dans la conception des gridshells est le manque de diversité des formes accessibles. En effet, bien que toute surface admette localement en tout point un réseau de Chebyshev, l'existence globale de ce type de coordonnées n'est possible que sur un ensemble restreint de surfaces. La recherche de conditions suffisantes pour l'existence globale de réseaux de Chebyshev est toujours d'actualité. Un des résultats de cette thèse est l'amélioration de ces conditions. Les possibilités d'améliorations en ce sens étant néanmoins limitées, nous élargissons la perspective en considérant des réseaux de Chebyshev avec singularités. Notre résultat principal est l'existence de réseaux de Chebyshev avec singularités coniques, lisses par morceaux, sur toute surface dont la courbure totale positive est inférieure à $2pi$ et dont la courbure totale négative est finie. Notre preuve est constructive, ce qui permet de déterminer ces réseaux dans des cas pratiques. Nous avons implémenté un cas particulier de notre algorithme dans le logiciel Rhinoceros et nous présentons des exemples de réseaux construits par cette méthode / Chebyshev nets are coordinate systems on surfaces obtained by pure shearing of a planar domain.These nets are used in particular to model gridshells, an architectural construction which is well-known for its low environmental impact. The main issue when designing a gridshell is the lack of diversityof the accessible shapes. Indeed, although any surface admits locally a Chebyshev net at any point, the global existence for these coordinate systems is only possible for a restricted set of surfaces. The research for sufficient conditions ensuring the global existence of Chebyshev nets is still ongoing. A result achieved in this thesis is an improvement on these conditions. Since the improvement in this direction seems to be rather limited, we broaden the perspective by introducing Chebyshev nets with singularities. Our main result is the existence of a global Chebyshev net with conical singularities on any surface with total positive curvature less than $2pi$ and with finite total negative curvature. Our proof is constructive, so that this method can be applied to practical cases. We have implemented a special instance of this algorithm in the software Rhinoceros and some discrete Chebyshev nets constructed using this method are presented

O presente trabalho consiste na apresentação da implementação de um software projetado para auxiliar o ensino de redes de Petri de alto nível. A partir da fundamentação sobre o assunto desenvolvida em cursos introdut6rios de modelagem de sistemas com redes de Petri foi especificado um sistema para ser usado em sala de aula. O sistema desenvolvido permite a demonstração das características gráficas e da semântica de alguns modelos tradicionais de redes de Petri, tais como redes condicao/evento, redes predicado-transição e redes coloridas. Redes de baixo nivel tambem podem ser demonstradas. O software foi elaborado de forma a permitir a utilização de redes já definidas em disquete. O usuário pode também definir novas redes utilizando o editor gráfico/compilador ou se valer de uma linguagem textual de baixo nível para descrever as redes. Após a obtenção da rede desejada, é possível a realização de demonstrações, simulando o funcionamento da mesma. O software permite ainda a execução de passos, o funcionamento "para trás" da rede e identifica, a cada estado alcançado, quais alterações estão habilitadas e quais estão em conflito. Um comando permite obter o caminho entre duas marcações da rede. O usuário pode selecionar regiões de interesse sobre a rede, que sera° mostradas com mais detalhe na tela. Usando o editor gráfico/compilador o usuário pode modificar redes durante o decorrer da apresentação. A interface com o usuário, voltada para o use em sala de aula, necessita como hardware um projetor de vídeo apropriado e um computador pessoal equipado com mouse. A utilização do compilador em sala de aula exige, no entanto, mais recursos computacionais que o simulador. Alguns modelos de redes de Petri não são suportados pelo compilador, mas podem ser implementados utilizando a linguagem de baixo nível do sistema. 0 usuário, professor ou aluno, encontrará neste trabalho instruções para o emprego pratico do sistema como instrumento para a realização de demonstrações didáticas. / This work describes the implementation of a software designed as a teaching aid for instructors of high-level Petri nets. A system for class-room use is described that is based on material developed during introductory courses of systems modelling with Petri nets. The class-room system permits the demonstration of the graphic properties and the semantics of some traditional nets, such as condition/event nets, predicate-transition nets and coloured nets, as well as low level nets. The software was designed to permit the use of nets already defined in diskettes. The user can define new nets using either the graphic editor/compiler or a low level textual language. Some models of Petri nets are not supported by the compiler, but can be implemented using the low level language. After obtaining the desired net, it is possible to perform demonstrations, simulating its operation.The software also allows step by step execution of nets, including backwards execution, and identifies, for every state, which alterations may happen and which are in conflict. A command permits the user to obtain the path between two markings of the net. The user may select regions of interest over the net, that will be shown with more detail in the screen. Using the graphic editor/compiler the user may modify the nets during the presentation. The hardware needs are a video projector and a personal computer equiped with a mouse.

A qualidade dos serviços de saúde tornou-se um tema relevante e cada vez mais esforços são dedicados para definir metodologias e ferramentas para medir e assegurar a qualidade. São exigidos novos métodos para aperfeiçoar os processos de saúde, garantindo assim uma alto padrão de qualidade utilizando os recursos disponíveis. A otimização da utilização destes recursos de forma a preservar a qualidade do atendimento bem como baixar os custos requer modelos rigorosos dos processos médicos. Neste contexto apresentamos LEMMA 2000 (Language for an Easy Medical Model Analysis) uma notação destinada a modelar processos médicos, desenvolvida em cooperação com o Politécnico de Milão.. Esta notação disponibiliza aos médicos elementos simples e intuitivos para representar os modelos de diagnóstico. Simultaneamente um modelo de Redes de Petri Temporizadas é gerado automaticamente. Deste modo os modelos de LEMMA podem ser validados e analisados através de simulações e testes.O objetivo desta dupla modelagem é permitir aos médicos ganhar todos os benefícios de uma notação formal sem a necessidade de conhecer esta notação abstrata. Os usuários administram os elementos mais simples da notação, enquanto redes de Petri asseguram formalidade e capacidades de validação. Desta maneira LEMMA integra notações formais e intuitivas superando os problemas de ambos enfoques. A definição da notação LEMMA 2000 foi apoiada pela implementação de um ambiente para projetar os modelos. Este ambiente além de permitir a administração dos elementos da notação menos formal permite a geração e analise dos modelos mais formais. / The quality of health services has become an important subject. Efforts have been dedicated more and more to define methodologies and tools to measure and to guarantee quality. People demand new methods in order to improve health processes. This way a high standard of quality is guaranteed by using available resources. The optimization of using these resources in such a way as to keep the quality of attendance as well as to reduce expenses, needs strict patterns of medical processes. In this context we present LEMMA 2000 a notation for modeling medical processes developed in co-operation with the Politecnico di Milano. This notation provides doctors with common and intuitive elements to represent the patterns of diagnoses. At the same time a model of Timed Petri nets is created automatically. Because of this the patterns of LEMMA can be validated and analysed through simulations and tests. The aim of this double modelling is to allow doctors to gain all the benefits of a formal notation without the need to know this abstract notation. The users manage the most simple elements of the notation while Petri nets guarantee formality and ways of validation. This way LEMMA integrates formal and intuitive notations overcoming problems of both focuses.The definition of LEMMA 2000 notation was supported by the implementation of an environment for projecting the patterns. This environment not only allows the management of the elements of the less formal notation but it also allows the creation and analysis of most formal patterns.

[pt] Este trabalho visa apresentar a integração de várias mídias de informação, como voz, texto, imagem e gráficos em um ambiente de troca de mensagens como a melhor resposta às solicitações de evolução de sistemas de troca de informação. Assim, será apresentado do LANBRETA-DMS (LAN-Based real Time Áudio-Data Message System), com ênfase na especificação de seus serviços, descrevendo-se a sintaxe do protocolo empregado e sua semântica, sendo esta última apresentada sob a forma de uma pseudo-linguagem de programação e sob a forma de redes de Petri. Uma implementação do LANBRETA-DMS, realizada nos laboratórios da PUC-RJ será também apresentada, seguindo- se proposições para extensões futuras. / [en] This work presents the integration of information media such as voice, text, imge and graphics in a message Exchange environment as the best answer to evolution of information Exchange systems. LANBRETA-DMS (LAN-Based Real Time Audio-Data Messege System) will be presented, with enphasis on the specification of its services, the protocol sintax used and its semantics, the latter being presented in a pseudo- programming language and in Petri Networks. An implementation of LANBRETA-DMS, made at PUC-RJ, will alos be introced, with some proposais for future extrensions following.

Coastal dolphin populations are indicators of environmental health and may be sensitive to anthropogenic influences. An observed increase in lesions during routine necropsies of dolphins prompted the first systematic health assessment of dolphins incidentally caught in shark nets off the KwaZulu-Natal coast. A detailed standard dissecting and sampling protocol for small cetaceans was developed for use in South Africa. Thirty five Indian Ocean bottlenose dolphins (Tursiops aduncus) and five Indo-Pacific humpback dolphins (Sousa chinensis), incidentally caught between 2010 and 2012, were subsequently evaluated by full necropsy and sampling using this protocol. All animals were considered to be in good nutritional condition, based on blubber thickness measurements and muscle condition. A large proportion of dolphins had lesions with parasitic aetiology, including pneumonia (34/40), bronchiolar epithelial mineralisation (33/40), gastroenteritis (28/40), hepatitis (24/39); endometritis (11/26), capsular inflammation of various abdominal and thoracic organs (30/40), and splenic capsular tags (18/40). Four parasite species (Halocercus sp., Crassicauda sp., Brachycladiinae, and Xenobalanus globicipitis) were recovered from six animals. Non-specific encephalomeningitis was found in 7/18 animals. Adrenal cortical hyperplasia (18/37,) possibly related to chronic stress, was also found, as well as myocardial fibrosis (10/39). Pulmonary pneumoconiosis and lymph node foreign material accumulation, possibly indicating exposure to polluted air, was seen in three animals. Lesions suggestive of morbillivirus, Toxoplasma gondii, or Brucella spp. tested negative on immunohistochemistry. The first confirmed cases of lobomycosis and sarcocystosis in South Africa were found. Most lesions were mild, although their high and apparently increasing prevalence may indicate a change in the host/parasite interface. This may be attributed to anthropogenic factors, such as stress or environmental pollution, suggesting degradation of the marine environment. This could also negatively impact human populations associated with the marine environment. The results indicate a need for continued health monitoring of coastal dolphin populations and for further research into disease pathophysiology and anthropogenic factors affecting these populations. This standard necropsy protocol will encourage a more complete health investigation of incidentally caught and stranded cetaceans in the region and will assist in expanding the current knowledge of diseases affecting dolphin populations in southern Africa. Furthermore, we provide valuable information regarding the baseline of disease affecting these populations, which may be used to determine and monitor temporal trends. / Dissertation (MSc)--University of Pretoria, 2013. / gm2014 / Production Animal Studies / unrestricted

In the past two decades, multi-agent systems (MAS) have emerged as a new paradigm for conceptualizing large and complex distributed software systems. A multi-agent system view provides a natural abstraction for both the structure and the behavior of modern-day software systems. Although there were many conceptual frameworks for using multi-agent systems, there was no well established and widely accepted method for modeling multi-agent systems. This dissertation research addressed the representation and analysis of multi-agent systems based on model-oriented formal methods. The objective was to provide a systematic approach for studying MAS at an early stage of system development to ensure the quality of design. Given that there was no well-defined formal model directly supporting agent-oriented modeling, this study was centered on three main topics: (1) adapting a well-known formal model, predicate transition nets (PrT nets), to support MAS modeling; (2) formulating a modeling methodology to ease the construction of formal MAS models; and (3) developing a technique to support machine analysis of formal MAS models using model checking technology. PrT nets were extended to include the notions of dynamic structure, agent communication and coordination to support agent-oriented modeling. An aspect-oriented technique was developed to address the modularity of agent models and compositionality of incremental analysis. A set of translation rules were defined to systematically translate formal MAS models to concrete models that can be verified through the model checker SPIN (Simple Promela Interpreter). This dissertation presents the framework developed for modeling and analyzing MAS, including a well-defined process model based on nested PrT nets, and a comprehensive methodology to guide the construction and analysis of formal MAS models.

Les systèmes logiciels complexes sont omniprésents dans notre vie quotidienne. De ce fait, un dysfonctionnement peut occasionner aussi bien une simple gêne qu'un danger mettant en péril des vies humaines. Le test est l'une des techniques les plus répandues (en particulier dans l'industrie) pour détecter les erreurs d'un système. Lorsque le cahier des charges d'un système est décrit par une spécification formelle, le test de conformité est utilisé pour garantir un certain niveau de confiance dans la correction d'une implémentation de ce système - dans ce cadre, la relation de conformité formalise la notion de correction. Cette thèse se focalise sur le test de conformité pour les systèmes concurrents. Le test de conformité pour les systèmes concurrents utilise principalement des modèles qui interprètent la concurrence par des entrelacements. Néanmoins, cette approche souffre du problème de l'explosion de l'espace d'états et elle n'offre pas la possibilité de tester certaines propriétés de la spécification telle que l'indépendance entre actions. Pour ces raisons, nous utilisons une sémantique d'ordres partiels pour la concurrence. De plus, nous proposons une nouvelle sémantique qui permet à certaines actions concurrentes d'être entrelacées et en force d'autres à être implémentées indépendamment. Nous proposons une généralisation de la relation de conformité ioco où les spécifications sont des réseaux de Petri et leur sémantique d'ordres partiels est donnée par leur dépliage. Cette relation de conformité permet de préserver l'indépendance, dans l'implémentation, des actions spécifiées comme concurrentes. Nous présentons un cadre de test complet pour cette relation. Nous définissons la notion de cas de test globaux gérant la concurrence, réduisant ainsi non seulement la taille des cas de test mais aussi celle de la suite de tests. Nous montrons comment les cas de test globaux peuvent être construits à partir du dépliage de la spécification en s'appuyant sur une traduction SAT, et nous réduisons le problème de la sélection de tests à la sélection d'un préfixe fini de ce dépliage : nous définissons différents critères de sélection à partir de la notion d'événement limite (cut-off event). Enfin, en supposant que chaque processus d'un système distribué possède une horloge locale, nous montrons que la conformité globale peut être testée dans une architecture de test distribuée en utilisant seulement des testeurs locaux ne communiquant pas entre eux. / Complex systems are everywhere and are part of our daily life. As a consequence, their failures can range from being inconvenient to being life-threatening. Testing is one of the most widely accepted techniques (especially in industry) to detect errors in a system. When the requirements of the system are described by a formal specification, conformance testing is used to guarantee a certain degree of confidence in the correctness of an implementation- in this setting a conformance relation formalizes the notion of correctness. This thesis focuses on conformance testing for concurrent systems. Conformance testing for concurrent system has mainly focused on models that interpret concurrency by interleavings. This approach does not only suf- fer from the state space explosion problem, but also lacks the ability to test properties of the specification such as independence between actions. For such reasons, we focus not only on partial order semantics for concurrency, but also propose a new semantics that allows to interleave some actions while forcing others to be implemented as independent. We propose a generalization of the ioco conformance relation, based on Petri nets specifications and their partial order semantics given by their unfoldings, preserving thus independence of actions from the specification. A complete testing framework for this conformance relation is presented. We introduce the notion of global test cases which handle concurrency, reducing not only the size of the test case, but also the number of tests in the test suite. We show how global test cases can be constructed from the unfolding of the specification based on a SAT encoding and we reduce the test selection problem to select a finite prefix of such unfolding: different testing criteria are defined based on the notion of cut-off events. Finally, we show that assuming each process of a distributed system has a local clock, global conformance can be tested in a distributed testing architecture using only local testers without any communication.

I engage in my dissertation thesis "Formation of strategy alliances into the segment of Information technologies" with problem of strategy alliance development into sector of information and communication technologies. Strategic alliances become an important factor impacting to the company behaviour, company competition advantages, new markets entering and dealing, sales strategy and channels definition as well as the form of marketing communication decision. The companies are deciding between two basic forms of behaviour, at current days. First form is focused to the independent strategy of compete fight, the second one is fosuced to the strategy of cooperation based on strategy allicances. I occupe by the questions delimitating development of strategy alliances, defining reasons and occasions of their establishement as well as current situation at this field, delimitate role and contribution of strategy partnership and aslo problems of practise application. The dissertation thesis are focused on the fullfilment of two basic goals, the congnitional and the inventive goal, buz first of all to the confirmation and/or disconfirmation of setted hypothesis. Due to the first congnitional goal I am analysing problems of multinational ICT companies strategy aliance development and then generalizing the problem. Due to the second inventive goal I am setting new metod of strategy aliance development. The sets hypothesis, as the main target of this work, openned the questions whether is possible to define the major tools and factors of strategy aliance success? If is possible to define the basic principles of strategy cooperation? Whether is possible to create simply applicable and in the same time higly effective method of strategy allicance developing?

京都大学 / 0048 / 新制・課程博士 / 博士(人間健康科学) / 甲第19644号 / 人健博第36号 / 新制||人健||3(附属図書館) / 32680 / 京都大学大学院医学研究科人間健康科学系専攻 / (主査)教授 高桑 徹也, 教授 三谷 章, 教授 浅野 雅秀 / 学位規則第4条第1項該当 / Doctor of Human Health Sciences / Kyoto University / DFAM