Submitted by Alice Araujo (alice.caraujo@ufpe.br) on 2017-12-04T18:10:07Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) bcfsDissertationvFinal5.pdf: 1922556 bytes, checksum: 47cd71107f5450414e172d96bd4454ed (MD5) / Made available in DSpace on 2017-12-04T18:10:07Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) bcfsDissertationvFinal5.pdf: 1922556 bytes, checksum: 47cd71107f5450414e172d96bd4454ed (MD5) Previous issue date: 2016-09-05 / Software Engineering faces challenges such as difficulty in understanding the user needs, ambiguous specifications, poorly defined requirements and therefore problems in interpreting the system requirements. Model-based testing (MBT) is presented as an alternative for solving these problems by using (semi-)formal methods, in the specification, modelling or analysis of requirements, as well as by automatically generating test cases. This work proposes and implements a test generation strategy from Natural Language (NL) requirements via translation into Coloured Petri Nets (CPN), an extension of Petri Nets that supports model structuring. This strategy extends previous work on the NAT2TEST framework, which involves syntactic and semantic analyses of NL requirements and the generation of Data-Flow Reactive System (DFRS) as an intermediate representation, from which target formal models can be obtained for the purpose of test case generation. Our contributions include a systematic translation of DFRSs into CPN models, besides a strategy for test generation. We illustrate our overall approach with a running example. Therefore, this work presents a variant for the NATural Language Requirements to TEST Cases (NAT2TEST) strategy, in which the Coloured Petri Nets (CPN) is used as an intermediate model. The NAT2TEST strategy, which is applicable to discrete or continuous systems, consists of five phases: syntactic and semantic analyses, DFRS generation, CPN generation, and generation of test cases. The approach proposed here, which is based on Petri Nets simulation, has as benefit the maturity of the theory and tools related to CPN. Moreover, there are available resources for analysing structural and behavioural properties of the model. The process is automated by the NAT2TEST tool until the DFRS generation. The model translation from the DFRS to the CPN is automated by Spoofax framework. Finally, the test cases generation occurs automatically via simulations held in the CPN Tools. Our strategy was evaluated considering examples from the literature (Vending Machine and Nuclear Power Plant) and the aerospace industry (Priority Control). We analysed performance and the ability to detect defects generated via mutation. In general, our strategy outperformed the considered baseline: random testing. We also compared our strategy with the CSP version. / A Engenharia de Software possui desafios clássicos como dificuldade no entendimento das necessidades dos usuários, especificações ambíguas, requisitos mal definidos e, portanto, problemas na interpretação destes. A utilização de testes baseados em modelos (MBT) apresenta-se como alternativa para solução destes problemas, através do uso de métodos (semi)formais, seja na especificação, modelagem ou análises de requisitos, bem como na geração automática de casos de testes. Este trabalho propõe e implementa uma estratégia de geração de testes a partir de requisitos escritos em linguagem natural (NL) através da tradução para modelos em Redes de Petri Colorida (CPN), uma extensão de Redes de Petri que incorpora estruturação de modelos. Esta estratégia estende um trabalho anterior (NAT2TEST framework), que envolve análises sintática e semântica de requisitos em linguagem natural (NL) e geração do modelo de sistemas reativos baseados em fluxos de dados (DFRS) como uma representação intermediária, a partir do qual outros modelos formais podem ser obtidos com o propósito de geração de casos de testes. Nossa contribuição inclui uma tradução sistemática de DFRSs para modelos CPN, assim como uma estratégia para geração de testes. Ilustramos nossa abordagem através de um exemplo prático. Assim sendo, este trabalho apresenta uma variante da estratégia NAT2TEST, na qual formalismo intermediário é Redes de Petri Colorida (CPN), sendo aplicável a sistemas discretos e contínuos, e que consiste de cinco etapas: análises sintática e semântica, gerações dos modelos DFRS e CPN e de casos de testes. A abordagem empregada, através da simulação de Redes de Petri, tem como benefícios a maturidade da teoria e das ferramentas associadas a CPN, além de permitir a análise de propriedades estruturais e comportamentais do modelo. A ferramenta NAT2TEST já automatiza a tradução de requisitos em linguagem natural na notação do DFRS. A tradução do modelo DFRS para o formalismo CPN é uma primeira contribuição do presente trabalho e foi automatizada através do ambiente Spoofax. A geração dos casos de testes foi desenvolvida, de forma automatizada, através de simulações realizadas na ferramenta CPN Tools. A estratégia aqui proposta foi avaliada considerando exemplos da literatura (Vending Machine (VM) e Nuclear Power Plant (NPP)) e da indústria aeroespacial (Priority Control (PC)). Foram analisados o desempenho e a capacidade de detectar defeitos gerados através de operadores de mutação. Em geral, a nossa estratégia apresentou melhores resultados do que a referência adotada: testes aleatórios. A estratégia também foi comparada com a versão que utiliza Communicating Sequential Processes (CSP) como modelo formal intermediário e apresentou melhor desempenho nos três estudos realizados. Em um deles, encontrou a mesma quantidade de defeitos, sendo superior nos demais.

Orientadores : Leo Pini Magalhães, Ivan Luiz Marques Ricarte / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-07-28T01:36:32Z (GMT). No. of bitstreams: 1 Raposo_AlbertoBarbosa_D.pdf: 11713768 bytes, checksum: 2dbdf2cc7f0274ac30ffe5cdae9cee99 (MD5) Previous issue date: 2000 / Resumo: A coordenação das interdependências entre atividades colaborativas é uma tarefa complexa, de difícil modelagem computacional. Este trabalho define uma série de interdependências que ocorrem freqüentemente entre tarefas colaborativas e apresenta um conjunto de mecanismos de coordenação para a especificação e controle da interação entre essas tarefas. Estes mecanismos são genéricos e podem ser reutilizados em uma série de ambientes colaborativos, tais como workflows interorganizacionais e ambientes virtuais colaborativos. A separação entre atividades (tarefas) e dependências (controladas pelos mecanismos de coordenação) permite o uso de diferentes políticas de coordenação em um mesmo ambiente colaborativo, sendo necessário apenas trocar os mecanismos de coordenação. Os mecanismos são modelados por redes de Petri, que oferecem um suporte matemático para análise e simulação do comportamento do ambiente colaborativo. Com o modelo baseado em redes de Petri, é possível prever e testar o comportamento de um ambiente de suporte ao trabalho colaborativo antes mesmo de sua implementação / Abstract: The coordination of interdependencies among activities in collaborative environments is a very important and difficult task. This work defines a group of interdependencies that frequently occurs among collaborative tasks and presents a set of coordination mechanisms for the specification and control of interaction among these tasks. These mechanisms are generic and can be reused in several collaborative environments, such as interorganizational workflows and collaborative virtual environments. The separation between activities (tasks) and dependencies (controlled by the coordination mechanisms) allows the use of different coordination policies in the same collaborative environment by changing the coordination mechanisms. These mechanisms are modeled using Petri nets, which have a strong theoretical support for analysis and simulation of the collaborative environment's behavior. Using the Petri nets based model, it is possible to anticipate and test the behavior of a computer supported collaborative system even before its implementation / Doutorado / Engenharia de Computação / Doutor em Engenharia Elétrica

Orientador: Leo Pini Magalhães / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-07-29T00:33:07Z (GMT). No. of bitstreams: 1 Bicho_AlessandrodeLima_M.pdf: 864359 bytes, checksum: 257c87945ab54bde180d6c2257f53372 (MD5) Previous issue date: 2001 / Mestrado

Orientador : Rafael Santos Mendes / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-07-29T01:59:29Z (GMT). No. of bitstreams: 1 Luders_Ricardo_D.pdf: 971778 bytes, checksum: 4356afeeb0fdd1b399f01103c6df108b (MD5) Previous issue date: 2001 / Doutorado

Orientador: Walter da Cunha Borelli / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-14T17:26:38Z (GMT). No. of bitstreams: 1 Damasceno_BereniceCamargo_M.pdf: 9724675 bytes, checksum: e2ac5ac37aa8889d89a0a897d68b38ed (MD5) Previous issue date: 1989 / Resumo: Não informado / Abstract: Not informed. / Mestrado / Mestre em Engenharia Elétrica

The aggregation hierarchy is one of the most significant data abstraction mechanisms that emerged as a result to semantic extensions to traditional systems analysis and design methods. The way inheritance works in this hierarchy is studied in this thesis. Special emphasis is placed on the behaviour of objects which are related via an aggregation hierarchy. A framework is introduced for capturing the behaviour of a system from the respective behaviour(s) of its components. This framework is based on a 3-level behaviour modelling hierarchy. One of the most significant contributions of this framework is the ability to apply inter-object interactions when building a behaviour model of a system. These interactions are significant in that they can yield totally distinct models of the systems functionality. Some of the notions that are supported by the behaviour modelling framework include unreachable and transient states, transition chains (cascades) and concurrency. The framework also enables the creation of behaviour model (semantic) hierarchies, wherein certain facets of the systems behaviour or functionality can be hidden (abstracted out) in a gradual fashion that suits the requirements of the problem domain. This creates what is effectively, distinct views of the behaviour or functionality of the system. The notions and concepts that are introduced here are verified and presented in a comprehensive case study that shows what can be achieved using these ideas. Suggestions are also made for future work which can help overcome some of the limitations introduced throughout this research.

Petri Nets are a formal, graphical and executable modeling technique for the specification and analysis of concurrent and distributed systems and have been widely applied in computer science and many other engineering disciplines. Low level Petri nets are simple and useful for modeling control flows but not powerful enough to define data and system functionality. High level Petri nets (HLPNs) have been developed to support data and functionality definitions, such as using complex structured data as tokens and algebraic expressions as transition formulas. Compared to low level Petri nets, HLPNs result in compact system models that are easier to be understood. Therefore, HLPNs are more useful in modeling complex systems. There are two issues in using HLPNs - modeling and analysis. Modeling concerns the abstracting and representing the systems under consideration using HLPNs, and analysis deals with effective ways study the behaviors and properties of the resulting HLPN models. In this dissertation, several modeling and analysis techniques for HLPNs are studied, which are integrated into a framework that is supported by a tool. For modeling, this framework integrates two formal languages: a type of HLPNs called Predicate Transition Net (PrT Net) is used to model a system's behavior and a first-order linear time temporal logic (FOLTL) to specify the system's properties. The main contribution of this dissertation with regard to modeling is to develop a software tool to support the formal modeling capabilities in this framework. For analysis, this framework combines three complementary techniques, simulation, explicit state model checking and bounded model checking (BMC). Simulation is a straightforward and speedy method, but only covers some execution paths in a HLPN model. Explicit state model checking covers all the execution paths but suffers from the state explosion problem. BMC is a tradeoff as it provides a certain level of coverage while more efficient than explicit state model checking. The main contribution of this dissertation with regard to analysis is adapting BMC to analyze HLPN models and integrating the three complementary analysis techniques in a software tool to support the formal analysis capabilities in this framework. The SAMTools developed for this framework in this dissertation integrates three tools: PIPE+ for HLPNs behavioral modeling and simulation, SAMAT for hierarchical structural modeling and property specification, and PIPE+Verifier for behavioral verification.

Orientador: Rafael Santos Mendes / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica e de Computação / Made available in DSpace on 2018-07-24T03:50:44Z (GMT). No. of bitstreams: 1 Magossi_JoseCarlos_D.pdf: 6761411 bytes, checksum: ceea1c2dd3d35ba4d2e536d090e00ab6 (MD5) Previous issue date: 1998 / Resumo: Aborda-se o problema de verificação de especificações e síntese de controladores em uma classe de sistemas dinâmicos a eventos discretos. Propõe-se uma nova lógica modal denominada lógica modal NK, e mostra-se que um conjunto de fórmulas nesta lógica é equivalente a um conjunto de fórmulas escritas no contexto da teoria de dióides. Desse modo, um sistema descritível por um grafo a eventos, que é modelado por um conjunto de equações num dióide apropriado, também é modelado por um conjunto de fórmulas da lógica modal NK. Então utiliza-se as técnicas de tableaux analíticos para desenvolver um algoritmo para decidir se uma especificação é satisfeita ou não. Quanto ao problema de síntese, a solução obtida pelo tableau analítico é utilizada para determinar as NK-fórmulas, e portanto o controlador, que tomará a especificação satisfeita. A principal vantagem deste inter-relacionamento de abordagens é permitir a utilização de técnicas da lógica modal, particularmente os tableaux analíticos, no tratamento de problemas de análise e síntese de controlad9res para sistemas a eventos discretos / Abstract: The problem of verification of a specification and controller synthesis in a class of discrete event dynamic systems is addressed. We propose a new propositional modallogic, named NK logic, and we show that a set of formulas of this logic is completely equivalent to a set of equations written in the context of the theory of dioids. Therefore, a system described by an event graph can be modeled by a set of formulas in NK logic. Then we use the technique of the analytic tableaux to develop an algorithm to decide if a specification, also expressed in NK logic, is satisfied. If a specification is not satisfied then there exists a solution for the equations written in dioid context that violates the specification. The method of analytic tableaux gives this solution. Conceming the synthesis problem, the solution obtained by the analytic tableau is used to determine the NK-formulas, and therefore the controller, that makes the specification be verified. The main advantage of this approach is allow us to use the technique of analytic tableaux to investigate problems of analysis and synthesis of controllers for discrete event systems / Doutorado / Doutor em Engenharia Elétrica

Orientador: Wagner Caradori do Amaral / Tese (doutorado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-15T16:56:04Z (GMT). No. of bitstreams: 1 Souza_JoaoNunesde_D.pdf: 12097520 bytes, checksum: 6aa96dc3547fd563a0ed50eb97d3a98c (MD5) Previous issue date: 1989 / Resumo: Neste trabalho propõe-se um estudo da representação hierárquica de conhecimento a partir dos conceitos básicos do 'lambda¿-cálculo tipado. A representação do conhecimento é feita por programas funcionais definidos como conjuntos de fórmulas do 'lambda¿-cálculo tipado. Os conjuntos de fórmulas são associados a critérios de derivação que determinam os argumentos das funções dos programas. estabelecendo o seqüenciamento da execução destas funções e possibilitando a derivação de novos conhecimentos. Propõe-se um conjunto de relações de complexidade entre as fórmulas do 'lambda¿-cálculo tipado. que se baseia em uma classificação destas fórmulas. A classificação se fundamenta na estrutura sintática dos símbolos para tipo associados às fórmulas. A ordem dos símbolos para tipo determina relações de ordem entre as fórmulas do 'lambda¿-cálculo tipado, definindo as relações de complexidade. As relações de complexidade são utilizadas em uma representação sintática das relações hierárquicas de complexidade do conhecimento representado em um sistema. Demonstra-se um conjunto de condições necessárias ... Observação: O resumo, na íntegra, poderá ser visualizado no texto completo da tese digital / Abstract: A knowledge hierarchic representation based on the typed 'lambda¿-calculus foundat ions is proposed in this work. The knowledge representation is based in functional programms defined as typed h-calculus formulas set. The formulas set is associated to derivation criterias that determines the programms functions arguments and the execution function sequence. A typed 'lambda¿-calculus formulas complexity relationship based on a typed h-calculus formulas classification is proposed. The classification is based on the formulas and type simbols sintat ic structure. The type simbols orders determines typed 'lambda¿-calculus formulas order relations wich define the complexity relationship. The complexity relationship is used to represent a sintatic representation of a knowledge system hierarchic relationship complexity ... Note: The complete abstract is available with the full electronic digital thesis or dissertations / Doutorado / Doutor em Engenharia Elétrica

Orientador: Shusaburo Motoyama / Dissertação (mestrado) - Universidade Estadual de Campinas, Faculdade de Engenharia Eletrica / Made available in DSpace on 2018-07-17T17:32:48Z (GMT). No. of bitstreams: 1 Tamura_RobertoToshiyuki_M.pdf: 5692280 bytes, checksum: 5060e1cac0598ce84d6c8f7ffee3b0b4 (MD5) Previous issue date: 1988 / Resumo: Não informado / Abstract: Not informed. / Mestrado / Mestre em Engenharia Elétrica