Sistemas Reativos caracterizam-se por reagir continuamente a estímulos externos e internos e controlar atividades humanas. A ocorrência de falhas nesses sistemas pode resultar em grandes prejuízos. Dessa forma, o uso de métodos e técnicas rigorosas para a especificação do comportamento desse tipo de sistema é essencial, buscando-se evitar inconsistências e ambigüidades no modelo. Redes de Petri é uma das técnicas que têm sido usadas para a especificação de sistemas reativos. Teste e validação são atividades essenciais na produção dessa classe de sistemas. Por isso, o critério Análise de Mutantes, um critério de teste baseado em erros normalmente aplicado ao teste de programas, tem sido explorado no contexto de teste de especificações de sistemas reativos. É necessário o desenvolvimento de ferramentas que apóiem sua utilização, visto que a aplicação manual do critério é impraticável. O objetivo deste trabalho é a implementação da ferramenta Proteum-RS/PN, que apóia a aplicação do critério Análise de Mutantes para validar especificações baseadas em Redes de Petri. / Reactive Systems are characterized by continuously reacting to external as well as internal stimuli and controlling human activities. In these systems, faults can result in large losses. The use of rigorous methods and techniques for the specification of their behavior is essential to avoid inconsistencies and ambiguities. Petri Nets have been used for reactive-system specification. The test and validation of the underlying model are essential activities for the production of such systems. Thus, the Mutant Analysis -- a fault-based criterion usually used for program testing -- has been explored in the context of specification testing. The development of tools to support its application is necessary, since its manual application is unrealistic. The objective of this work is the implementation of Proteum-RS/PN, a testing tool which supports the application of Mutant Analysis criterion to validate Petri-Nets based specifications.

Thesis. 1976. Ph.D.--Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. / Microfiche copy available in Archives and Engineering. / Vita. / Bibliography: leaves 188-193. / Ph.D.

Neste trabalho apresenta-se um estudo do comportamento estrutural de cestas protendidas, tendo em vista a sua utilização em coberturas pênseis de grandes áreas livres. A partir da Técnica do Meio Contínuo obtêm-se as equações que permitem analisar as cestas protendidas quanto a esforços e deslocamentos. Fazem-se considerações sobre o sistema de equações encontrado visando a sua resolução mediante o emprego de programa computacional como instrumento de cálculo. Apresentam-se exemplos numéricos e os resultados são comparados com os obtidos em outros trabalhos. Fazem-se algumas considerações a respeito do projeto e do cálculo de cestas protendidas, além de algumas indicações sobre a continuidade da pesquisa. / This work presents a continuous medium method analysis of cable nets and their applications as suspended roofs for large free spans. lnitially the theory of the method is presented and later applied to get the system of differential equation that represents the problem. Finally this system is numerically solved with computational procedures. Some examples are presented and the results compared with those obtained with others methods and numerical procedures. Some analysis and design considerations and further developments in this subject are also included.

Aujourd'hui en France, l'évaluation de la performance de stratégies de sécurité à déployer pour mettre un bâtiment en sécurité vis-à-vis de l'incendie repose sur une étude d'ingénierie en sécurité incendie. Cette étude a pour objectif l'estimation du risque incendie pour différentes stratégies, et pour des scénarios d'incendies jugés pertinents. Pour parvenir à cette estimation, le Centre Scientifique et Technique du Bâtiment français (CSTB) a mis au point un outil de simulation appelé SCHEMA-SI. Cet outil utilise des réseaux de Petri prédicat-transition différentiels orientés objets et des simulations de Monte Carlo pour générer de multiples scénarios d'incendie. Ces scénarios sont ensuite utilisés pour évaluer le risque incendie encouru avec une stratégie de sécurité. La stratégie est alors jugée d'autant plus performante que le risque incendie est faible. L'objectif de la thèse consiste à contribuer au développement d'une méthode d'analyse de risque incendie utilisant l'outil de simulation SCHEMA-SI. La réflexion a débuté par la définition de ce que devrait être cette méthode. A ce stade, il est apparu que l'une des difficultés que la méthode doit surmonter est celle de la mise en donnés du problème par un groupe d'acteurs impliqués dans la sécurité incendie du bâtiment étudié. Pour résoudre cette difficulté, une méthode de modélisation spécifique a été construite. Cette méthode, baptisée ISI-Systema, repose sur deux fondements principaux : d'une part, un langage graphique de modélisation permettant au groupe d'acteurs de réfléchir à la mise en données du problème en s'appuyant sur une approche systémique ; d'autre part, une démarche de traduction des modèles graphiques obtenus avec le langage systémique en réseaux de Petri compatibles avec SCHEMA-SI.Enfin, une application pratique de cette méthode de modélisation est proposée. / Nowadays in France, building fire safety strategy performance analysis relies on a fire engineering study. This kind of study aims at calculating fire risk for several strategies and for fire scenarios judged as relevant. In order to achieve risk calculation, the French Scientific and technical Building Center (CSTB) has developed a simulation tool called SCHEMA-SI. This tool is based on object-oriented differentiai predicate-transition Petri nets and on Monte Carlo simulations and is built to generate a large number of fire scenarios. Obtained scenarios are hence used to evaluate fire risk related to the strategy to evaluate. The lower the fire risk is obtained, the more efficient the strategy is considered. This thesis aims at contributing to the development of a SCHEMA-SI based fire risk assessment method. This thesis starts by a definition of what this method should be. At this stage, it appears that one of the difficulties to overcome is the one of the problem definition by a group of fire safety concerned people. In arder to solve this difficulty, a modeling method has been developed. This method, so-called ISI-Systema, relies on two main basements: in on hand, on a graphic modeling language created to allow a group of people to think about the problem definition by using a systemic approach ; on the other hand, on a SCHEMA-SI compatible Petri net - graphic model translation procedure. At last, a case study is proposed.

This research addressed the design and implementation of a polynomial-complexity deadlock avoidance controller for a flexible manufacturing cell modeled using Colored Petri Nets. The cell model is robust to changes in the part types to be manufactured in the system and is automatically generated using the interaction of the resources in the cell and the technological capabilities of the machines. The model also captures dynamic routing flexibility options. The framework introduced separates the cell model from the control logic allowing the system designer to implement and test various control algorithms using the same cell model. The controller adopts the neighborhood deadlock avoidance policy to resolve deadlocks and control the resource allocation decisions within the system. The evaluation of the performance of systems controlled by not maximally permissive algorithms is important in determining the applicability of the control algorithms. There are many polynomial time deadlock avoidance algorithms proposed for the control of general resource allocation systems. However, the permissiveness of these algorithms is not quantified and the applicability of these algorithms in terms of effective resource utilization remains unanswered. The performance of automated manufacturing cells controlled using the neighborhood deadlock avoidance policy is benchmarked by comparing its performance with other control policies.

The Resource Reservation Protocol (RSVP) is one of the proposals of the Internet Engineering Task Force (IETF) for conveying Quality of Service (QoS) related information in the form of resource reservations along the communication path. The RSVP specification (i.e. Request for Comments 2205) provides a narrative description of the protocol without any use of formal techniques. Thus, some parts of the document may be ambiguous, difficult to understand, and imprecise. So far, RSVP implementations have provided the only mechanism for validating. The cost for fixing errors in the protocol found in the implementation can be high. These disadvantages together with the fact that RSVP is complex make it a good target for formal specification and verification. This thesis formally defines the RSVP Service Specification, models RSVP using a formal method known as Coloured Petri Nets (CPNs) and attempts to verify the model. The following steps summarise the verification process of RSVP. Firstly, the RSVP service specification is derived from the protocol description and modelled using CPNs. After validating the model, the service language, which defines all the possible service primitive occurrence sequences, is generated from the state space of the model by using automata reduction techniques that preserve sequences. Secondly, RSVP is modelled using CPNs. The model is analysed for a set of behavioural properties. They include general properties of protocols, such as correct termination, and a set of new properties defined in this thesis, which are particular to RSVP. The analysis is based on the state space method. The properties are checked by querying the state graph and checking reachability among multiple nodes of its associated Strongly Connected Component (SCC) graph. As a first step, we analyse RSVP under the assumption of a perfect medium (no loss or duplication) to ensure that protocol errors are not hidden by rare events of the medium. The state space is reduced to obtain the sequences of service primitives allowed by RSVP known as the protocol language. Then, the protocol language is compared with the service language to determine if they are equivalent. The desired properties of RSVP are proved to be satisfied by the RSVP CPN model, so that the features of RSVP included in the CPN model operate as expected under our modelling and analysis assumptions. Also, the language analysis results show that RSVP service primitive occurrence sequences generated by the RSVP model are included in the proposed model of the service specification. However, some service primitive occurrence sequences generated from the service specification model are not in the protocol language. These sequences were analysed. There is strong evidence to suggest that these sequences would also appear in the protocol if the capacity of the medium in the RSVP model was marginally increased. Unfortunately, the standard reachability analysis tools would not handle this case, due to state space explosion. / Thesis (PhD)--University of South Australia, 2003

The Synchronize Choice Petri net, a subclass of Petri nets that is constructed based on special structural objects, can improve analytical power to make solving the behavioral problems of Petri nets practically possible. The fact that proving liveness and verifying reachability of a Synchronize Choice Petri net are feasible may lead to several applications. This thesis contributes to one of the applications: building a dynamic key exchange mechanism embedded in Virtual Private Network products by applying Synchronize Choice Petri nets. 　　Based on modern symmetric-key algorithms, such as DES, the dynamic key exchange mechanism enables two communicating sides to use the changing keys to encrypt or decrypt messages correctly without requiring any key transmission during the communication session after the initiation. A proper use of the mechanism is to be integrated with Virtual Private Network products to make the information transmitting between two peers more confidential.

<p>Embedded systems are used in a wide spectrum of applications ranging from home appliances and mobile devices to medical equipment and vehicle controllers. They are typically characterized by their real-time behavior and many of them must fulfill strict requirements on reliability and correctness.</p><p>In this thesis, we concentrate on aspects related to modeling and formal verification of realtime embedded systems.</p><p>First, we define a formal model of computation for real-time embedded systems based on Petri nets. Our model can capture important features of such systems and allows their representations at different levels of granularity. Our modeling formalism has a welldefined semantics so that it supports a precise representation of the system, the use of formal methods to verify its correctness, and the automation of different tasks along the design process.</p><p>Second, we propose an approach to the problem of formal verification of real-time embedded systems represented in our modeling formalism. We make use of model checking to prove whether certain properties, expressed as temporal logic formulas, hold with respect to the system model. We introduce a systematic procedure to translate our model into timed automata so that it is possible to use available model checking ools. Various examples, including a realistic industrial case, demonstrate the feasibility of our approach on practical applications.</p>

<p><strong>Background: </strong>The development of the IT-industry, where new technologies and new services continually arise, has led to new players with different specializations. The increased degree of specialization means that these players need to cooperate with each other in different types of projects.</p><p><strong>Problem definition: </strong>What factors are important in a project to achieve the objectives as quickly as possible? More players should lead to cooperation difficulties, how can you coordinate in the best possible way? Today, it is desirable for all parties in the project to shorten down the lead time.</p><p><strong>Purpose: </strong>The main purpose is to explore the different factors that affects the project's lead time concerning broadband installation. The part purpose, is to analyze and assess the conditions for cooperation between different players in the project for broadband installation and to provide a recommendation.</p><p><strong>Method: </strong>In order to answer the problem definition, the paper is structured around a qualitative approach with interviews to obtain data. Mostly, the used data comes from primary sources with an extension of secondary sources.</p><p><strong>Theories: </strong>Theories that are used in the paper are: Communication Process, Communication Plan, Project Planning & Project Plan, Efficiency through collaboration, Communication in a network.</p><p><strong>Empiric: </strong>Empirical data consists of primary data collected through interviews.</p><p><strong>Analysis:</strong> The analysis is based on the variables from the theoretical frame of reference; Communications, Planning, Interaction & Information. From these variables, empirical data are analyzed in relation to the theory.</p><p><strong>Conclusion:</strong> In the conclusion, the authors discuss about the projects process which is described in the paper. The authors have concluded that; communication, planning and collaboration plays a major role in order to shorten down the lead times for the project. Cooperation beyond enterprise boundaries becomes necessary.</p>

<p>In recent years, there has been much advancement in the area of verification of infinite-state systems. A system can have an infinite state-space due to unbounded data structures such as counters, clocks, stacks, queues, etc. It may also be infinite-state due to parameterization, i.e., the possibility of having an arbitrary number of components in the system. For parameterized systems, we are interested in checking correctness of all the instances in one verification step. </p><p>In this thesis, we consider systems which contain both sources of infiniteness, namely: (a) real-valued clocks and (b) parameterization. More precisely, we consider two models: (a) the timed Petri net (TPN) model, which is an extension of the classical Petri net model; and (b) the timed network (TN) model in which an arbitrary number of timed automata run in parallel. </p><p>We consider verification of safety properties for timed Petri nets using forward analysis. Since forward analysis is necessarily incomplete, we provide a semi-algorithm augmented with an acceleration technique in order to make it terminate more often on practical examples. Then we consider a number of problems which are generalisations of the corresponding ones for timed automata and Petri nets. For instance, we consider zenoness where we check the existence of an infinite computation with a finite duration. We also consider two variants of boundedness problem: syntactic boundedness in which both live and dead tokens are considered and semantic boundedness where only live tokens are considered. We show that the former problem is decidable while the latter is not. Finally, we show undecidability of LTL model checking both for dense and discrete timed Petri nets. </p><p>Next we consider timed networks. We show undecidability of safety properties in case each component is equipped with two or more clocks. This result contrasts previous decidability result for the case where each component has a single clock. Also ,we show that the problem is decidable when clocks range over the discrete time domain. This decidability result holds when the processes have any finite number of clocks. Furthermore, we outline the border between decidability and undecidability of safety for TNs by considering several syntactic and semantic variants.</p>