Propõe-se uma estratégia de modelagem e de análise formal de políticas de segurança para sistemas baseados em fluxos de trabalho (workflows) e contendo regras que envolvam aspectos de lógica de negócios. Verifica-se com o auxílio de uma política de exemplo que a estratégia proposta resulta em modelos amplamente capazes de expressar restrições lógicas em função de parâmetros de negócio sem comprometer a viabilidade de suas análises. A modelagem baseia-se no uso de um metamodelo definido a partir da identificação das entidades que caracterizam o estado de proteção de um sistema e representado na forma de uma rede de Petri colorida. Por meio da escrita de predicados para consulta sobre o espaço de estados da rede de Petri, verifica-se o atendimento às regras de segurança no modelo formal. A tratabilidade da análise é garantida pela adoção de um paradigma diferenciado principalmente pela busca de ramos inseguros em vez de nós inseguros no espaço de estados e por explorar a natureza independente entre serviços de negócio distintos, expressa por restrições ao fluxo de informação no metamodelo. Tais restrições permitem que a análise seja fracionada evitando o problema da explosão de estados. O exemplo discutido de modelagem e análise de um sistema de serviços bancários online fornece evidências suficientes para atestar a aplicabilidade do método à validação de políticas de segurança para sistemas reais. / A strategy is proposed for the formal modeling and analysis of workflow- -based security policies having rules which involve aspects of business logic. Aided by an example of security policy, the proposed strategy is shown to lead to models widely capable of expressing logical restrictions as functions of business parameters without compromising the feasibility of its analyses. The modeling is based on the usage of a metamodel defined from the identification of the entities that characterize the protection state of a system, and represented as a colored Petri net. By writing predicates for querying the Petri net state-space, compliance with security rules at the formal model is verified. The feasibility of the analysis is ensured by the adoption of a paradigm distinguished mainly for the search for insecure branches rather than insecure nodes in the state-space, and for exploiting the independent nature among different business services, expressed by restrictions to the information flow within the metamodel. Such restrictions allow the analysis to be fractioned, avoiding the state explosion problem. The example provided of modeling and analysis of an online banking services system offers enough evidence to attest the applicability of the method to the validation of security policies for real-world systems.

As importantes transformações das organizações nos últimos anos mostram que diferentes princípios de qualidade, competitividade e inovação devem ser conjugados para o projeto de sistemas de controle de sistemas produtivos. Esta abordagem, que traz benefícios às organizações, é viável em virtude da evolução das estratégias de integração e da tecnologia da informação. A partir da norma em elaboração ANSI/ISA S95, esta dissertação desenvolve procedimentos para definição do escopo funcional, requisitos e modelagem para o projeto de sistemas de controle de sistemas produtivos integrados à organização, atuando de forma estruturada, em conformidade com padrões técnicos de automação e engenharia de requisitos. Como resultados, estabelece procedimentos para o início do projeto que definem o escopo funcional do sistema de controle de sistemas produtivos integrado à gestão da organização. A seguir, estes procedimentos estabelecem os domínios semânticos dos subsistemas necessários para o desempenho de suas funções, acompanhados das respectivas linguagens de modelagem. A dissertação completa-se com a modelagem dos subsistemas através do E-MFG com comunicadores, modelagem esta que suporta os padrões existentes de programação da automação. Neste contexto, parte-se dos requisitos de cada subsistema coletados por uma versão modificada do caso de uso da UML, convertidos finalmente para o E-MFG com comunicadores. / The important changes that are happening inside organizations show that different principles of quality, innovation and competition should be combined during the design of control system of production systems. This approach is possible thanks to the evolution of integration strategy and information technology, generating benefits to organizations. Procedures are established to define system’s functional scope, requirements and models, based on the integrated approach of ANSI/ISA S95 standard. The procedures are developed by a structured process and according to automation standards and requirements engineering. The work’s first result is a procedure that defines a functional scope for control system design of production systems integrated with organization. As a second result, procedures help to define semantic domains of all subsystems needed to develop control system functions, as well as the modeling techniques for each domain. The result is complemented by modeling subsystems using an extended version of Mark Flow Graph (E-MFG with communicators). This task has the assistance of a modified use case version from “Unified Modeling Language” to collect requirements before modeling.

Submitted by admin tede (tede@pucgoias.edu.br) on 2018-11-08T18:17:38Z No. of bitstreams: 1 JULIANO RESENDE BUCCHIANDERI.pdf: 6086819 bytes, checksum: ec188a1a0edcce38757a6e0f604df66d (MD5) / Made available in DSpace on 2018-11-08T18:17:38Z (GMT). No. of bitstreams: 1 JULIANO RESENDE BUCCHIANDERI.pdf: 6086819 bytes, checksum: ec188a1a0edcce38757a6e0f604df66d (MD5) Previous issue date: 2018-09-11 / The appropriated and secure supply of electrical energy directly impacts on the present society. The increase in demand favors the growth of electrical systems, especially in distribution networks and substations, since they are responsible for lowering the electrical voltage, allowing energy distribution to the population. To keep distribution networks and substations running, without interruption or discontinuity, is utmost importance for the maintenance of electric power supply, and it is necessary to implement means to locate and improve the electrical protections in order to reduce failures or to suspend the electricity distribution. Distribution failures may result from lightning, overcurrent, short circuits, overvoltages, oil leakage on transformers, impedance failure etc. The present work presents the problem of possible defects that result in the substation power blackout, and aims to reduce the amount and frequency of substation power blackouts, contributing to the increase in industrial production. In this regard, qualitative and quantitative models using Petri nets of an electrical substation of distribution were developed, using simulation scenarios to indicate possible improvements in the electrical protections, reducing the inaccuracies and interruptions. / O fornecimento adequado e seguro de energia elétrica impacta diretamente na sociedade atual. O aumento da demanda torna favorável o crescimento dos sistemas de eletricidade, sobretudo nas redes e subestações de distribuição, pois estas são responsáveis por rebaixar a tensão elétrica, permitindo assim distribuição de energia para a população. Manter as redes e subestações de distribuição funcionando, sem interrupções ou descontinuidade, é de suma importância para a manutenção do fornecimento de eletricidade, sendo necessário implementar meios para localizar e melhorar as proteções elétricas afim de diminuir as falhas ou a suspensão da distribuição desta. As falhas da distribuição podem resultar de descargas atmosféricas, sobrecorrente, curtoscircuitos, sobretensões, vazamento de óleo nos transformadores, falha de impedância etc. O presente trabalho expõe o problema dos possíveis defeitos que resultam no desligamento da subestação e objetiva reduzir a quantidade e a frequência dos desligamentos da subestação, colaborando para o aumento na produção industrial. Para isso, desenvolveu modelos qualitativos e quantitativos utilizando redes de Petri de uma subestação elétrica de distribuição, utilizando cenários de simulação para apontar possíveis melhorias nas proteções diminuindo as incorreções e interrupções.

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.

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>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>