Made available in DSpace on 2016-04-29T14:23:40Z (GMT). No. of bitstreams: 1 Jose Valdvogel de Almeida Junior.pdf: 1664725 bytes, checksum: b5162f7ac0d53d0a3c9e995e1e643e18 (MD5) Previous issue date: 2015-11-19 / The component-based software development has proven effective for implementation in various fields of application, but still insufficient to create reusable and flexible parts. Processes and methods have been developed in order to address special care in this context. However, none of the proposed methods shows a simple specification of building blocks. To address this limitation we propose in this research work a split between the static and dynamic elements that make up the nature of an assembled component in a set of steps with application techniques using the best practices of software engineering. As a result, we reach the Component Specification method capable of generating well-designed models for building reusable and flexible software parts. A case study helps to illustrate the application of the method in an application context / O desenvolvimento de software baseado em componentes tem se provado efetivo para a implementação em diversos domínios de aplicação, mas ainda insuficiente para a criação de peças reusáveis e flexíveis. Processos e métodos foram desenvolvidos no intuito de endereçar cuidados especiais nesse contexto. No entanto, nenhum dos métodos propostos demonstra uma forma simples de especificação dos blocos construtores. Para tratar essa limitação propomos nesse trabalho de pesquisa uma divisão entre os elementos estáticos e dinâmicos que compõem a natureza de um componente reunidos em um conjunto de passos com aplicação de técnicas que utilizam as boas práticas da engenharia de software. Como resultado, chega-se ao Método de Especificação de Componentes capaz de gerar modelos bem elaborados para construção de peças de software reusáveis e flexíveis. Um estudo de caso ajuda a ilustrar a aplicação do método em um contexto de aplicação

Tese de mestrado integrado. Engenharia Electrónica e de Computadores. Faculdade de Engenharia. Universidade do Porto. 2012

Submitted by Diogo Barreiros (diogo.barreiros@ufba.br) on 2017-02-17T16:37:53Z No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Approved for entry into archive by Vanessa Reis (vanessa.jamile@ufba.br) on 2017-02-21T11:53:04Z (GMT) No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / Made available in DSpace on 2017-02-21T11:53:04Z (GMT). No. of bitstreams: 1 barboza2006.pdf: 716139 bytes, checksum: 56397fad812dffadf11ce4841ed6c59c (MD5) / O termo IEEE 802.11 diz respeito a uma família de especificações que buscam obter conectividade sem fio para estações fixas, portáveis e móveis em uma rede local. Redes IEEE 802.11 têm, recentemente, despertado interesse como tecnologia de suporte para a comunicação em aplicações sem fio na automação, em particular em aplicações de chão de fábrica e de controle de plantas, onde, muitas vezes, requisitos de tempo-real e requisitos de confiabilidade são necessários. Neste contexto, o uso de métodos formais permite a obtenção de um conhecimento mais preciso sobre as propriedades do protocolo bem como a especificação e verificação destas propriedades. Este trabalho apresenta uma especificação e verificação formal da função de controle de acesso ao meio da sub-camada MAC do padrão IEEE 802.11 usando UPPAAL, um verificador de modelos gratuito, que suporta os conceitos de relógios e tempo. O uso do UPPAAL permitiu considerar, dentro da modelagem, as características temporais do protocolo. A verificação procurou identificar uma série de propriedades que fornecesse aos projetistas de aplicações e sistemas de tempo-real um conjunto mínimo de garantias relativas aos canais de comunicação. Entre as propriedades verificadas, destacamos a habilidade das estações possuírem acesso ao meio dentro de um tempo finito e conhecido e, portanto, a adequação do protocolo como suporte a aplicações que necessitem de garantias temporais.

Submitted by João Bretas de Araujo (joaobretas@fgvmail.br) on 2010-12-22T14:27:41Z No. of bitstreams: 1 Dissertacao - Joao Bretas.pdf: 1174985 bytes, checksum: 2d443b4f657b8cbc7ff6798802dd1bd2 (MD5) / Approved for entry into archive by Andrea Virginio Machado(andrea.machado@fgv.br) on 2010-12-22T16:45:23Z (GMT) No. of bitstreams: 1 Dissertacao - Joao Bretas.pdf: 1174985 bytes, checksum: 2d443b4f657b8cbc7ff6798802dd1bd2 (MD5) / Made available in DSpace on 2010-12-28T16:33:30Z (GMT). No. of bitstreams: 1 Dissertacao - Joao Bretas.pdf: 1174985 bytes, checksum: 2d443b4f657b8cbc7ff6798802dd1bd2 (MD5) Previous issue date: 2010-09-30 / The concept of stochastic discount factor pervades the Modern Theory of Asset Pricing. Initially, such object allows unattached pricing models to be discussed under the same terms. However, Hansen and Jagannathan have shown there is worthy information to be brought forth from such powerful concept which undelies asset pricing models. From security market data sets, one is able to explore the behavior of such random variable, determining a useful variance bound. Furthermore, through that instrument, they explore one pitfall on modern asset pricing: model misspecification. Those major contributions, alongside with some of its extensions, are thoroughly investigated in this exposition. / O conceito de fator estocástico de desconto permeia a Teoria Moderna de Apreçamento de Ativos. A princípio, tal objeto permite homogeneização na discussão sobre modelos de apreçamento. No entanto, Hansen e Jagannathan mostraram que há mais a ser extraído desse poderoso conceito subjacente aos modelos. A partir de dados, estudam limites do comportamento dessa variável aleatória, determinando cotas inferiores para suas variâncias. Além disso, com aquele instrumento, exploram as fragilidades da modelagem em finanças como erros de especificação. Essas contribuições e algumas de suas extensões são investigadas nessa dissertação.

Submitted by Rafael Silva Santos (rafael.silva.sts@gmail.com) on 2018-04-19T01:03:05Z No. of bitstreams: 1 Dissertacao - Rafael Silva Santos - vDeposito.pdf: 42155755 bytes, checksum: fb36b8d70ad22da512d7f23dc3a13691 (MD5) / Approved for entry into archive by Elza Mitiko Sato null (elzasato@ibilce.unesp.br) on 2018-04-19T14:25:43Z (GMT) No. of bitstreams: 1 santos_rs_me_sjrp.pdf: 42155755 bytes, checksum: fb36b8d70ad22da512d7f23dc3a13691 (MD5) / Made available in DSpace on 2018-04-19T14:25:44Z (GMT). No. of bitstreams: 1 santos_rs_me_sjrp.pdf: 42155755 bytes, checksum: fb36b8d70ad22da512d7f23dc3a13691 (MD5) Previous issue date: 2018-03-27 / Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES) / Funções de transferência (FTs) são uma parte crucial do processo de exploração volumétrica em Visualização Direta de Volumes. Nesse processo, FTs desempenham duas tarefas principais: a classificação de materiais e o mapeamento de informações presentes nos dados para propriedades visuais. A busca por uma solução que lide com ambas as tarefas envolve uma série de fatores que, em conjunto, são um dos maiores desafios de visualização volumétrica. Neste trabalho, propomos uma abordagem de exploração que tem por objetivo envolver todo escopo e simplificar tanto a definição de FTs multidimensionais quanto a manipulação de datasets. A abordagem se organiza em três componentes: uma heurística baseada em entropia e correlação que guia a seleção de atributos para formação do espaço de entrada; um método de classificação que emprega a técnica de redução de dimensionalidade FastMap e a técnica de agrupamento DBSCAN para proporcionar a descoberta semiautomática de características volumétricas; e uma interface simplificada que, atrelada ao método de classificação, produz um gráfico de dispersão 2D de características para a exploração do volume. Inicialmente, o usuário deve analisar o ranking de atributos para formar um espaço multidimensional. Depois, deve escolher parâmetros para gerar o gráfico de características. Finalmente, deve navegar por esse gráfico a fim de identificar materiais ou estruturas relevantes. Nos experimentos realizados para avaliar a abordagem, os mecanismos disponibilizados permitiram encontrar e isolar de forma efetiva características inseridas em todos os datasets investigados. Aponta-se ainda como contribuição o baixo custo computacional, na prática, a complexidade de tempo do método de classificação é de O (n log n). O tempo de execução foi inferior a 11 segundos, mesmo quando datasets formados por cerca de 10 milhões de instâncias e com mais de 10 dimensões são utilizados. / Transfer functions (TFs) are a crucial part of the volume exploration process in Direct Volume Rendering. In this process, TFs perform two main tasks: material classification and mapping of information to visual properties. The search for a solution that copes with both tasks involves a number of factors that, together, is one of the greatest challenges of volume visualization. In this work, we propose an exploration approach that aims to involve the entire scope and a simplify both the definition of multidimensional TFs and the manipulation of datasets. The approach is organized into three components: a heuristic based on entropy and correlation that guides the selection of attributes to conceive the input space; a classification method, which uses the dimensionality reduction technique FastMap and the clustering technique DBSCAN to provide a semiautomatic features finding; and a simplified interface that, linked to the previous method, provide a 2D scatter plot of features for volume exploration. Initially, the user must analyze at the ranking of attributes to form a multidimensional space. Afterwards, it must choice parameters to generate the scatter plot. Finally, it must navigate through this chart in order to reveal relevant materials and features. In the experiments performed to evaluate the approach, the available mechanisms allow to effectively find and isolate features inserted in all investigated datasets. It is also pointed out as contribution a low computational cost, in practice the time complexity of the classification method is O(n log n). The runtime was less than 11 seconds, even when datasets formed by about 10 million instances and with more than 10 dimensions are used.

Um novo modelo para a especificação de hiperdocumentos denominado HMBS - Hyperdocument Model Based on Statecharts - é proposto. O HMBS adota como modelo formal subjacente a técnica Statecharts, cuja estrutura e semântica operacional são utilizadas para especificar a estrutura organizacional e a semântica de navegação de hiperdocumentos grandes e complexos. A definição do HMBS, bem como a semântica de navegação adotada, são apresentadas. Na definição apresenta-se como o modelo permite separar as informações referentes a estrutura organizacional e navegacional das representações físicas do hiperdocumento. Também são discutidas características do modelo que possibilitam ao autor analisar a estrutura do hiperdocumento, encorajando a especificação de hiperdocumentos estruturados. Para provar e validar a viabilidade prática do uso do HMBS num contexto real foi desenvolvido um ambiente de autoria e navegação de hiperdocumentos denominado HySCharts - Hyperdocumenf System based on Statecharts. Esse ambiente fornece facilidades de prototipação rápida e simulação interativa de hiperdocumentos. Para ilustrar como o modelo HMBS e o HySCharts podem ser utilizados no contexto de uma abordagem de projeto sistemática é utilizada como estudo de caso a especificação de um hiperdocumento que apresenta o Parque Ecológico de São Carlos / A new model for hyperdocument specification called HMBS - Hyperdocument Model Based on Statecharts - is proposed. HMBS uses the Statechart formalism as its underlying model. Statecharts structure and operational semantics are used to specify the organizational structure and the browsing semantics of large and complex hyperdocuments. The definition of HMBS is presented and its browsing semantics is described. It is shown how the model allows the separation of information related to the organizational and navigational structure from the hyperdocument\'s physical representation. Model features that allow authors to analyze the hyperdocument structure, encouraging the specification of structured hyperdocuments are also discussed. As a proof of concept and also to evaluate the feasibility of using HMBS in real-life applications a system called HySCharts - Hyperdocument System based on StateCharts - was developed. HySCharts is composed by an authoring and a browsing environments, supporting rapid prototyping and interactive simulation of hyperdocuments. A case study is presented that uses the specification of a hyperdocument introducing the Ecological Park of São Carlos to illustrate the use of HMBS and of the HySCharts environment integrated into a systematic design approach

O desenvolvimento de arquiteturas de controle para veículos submarinos é uma tarefa complexa. Estas podem ser caracterizadas pelos seguintes atributos: tempo real, multitarefa, concorrência e comunicações distribuídas em rede. Neste cenário, existem múltiplos processos sendo executados em paralelo, possivelmente distribuídos, e se comunicando uns com os outros. Neste contexto, o modelo comportamental pode levar a fenômenos como deadlocks, livelocks, disputa por recursos, entre outros. A fim de se tentar minimizar os efeitos de tais dificuldades, neste trabalho será apresentado um método para checagem de modelos de arquiteturas de controle de veículos submarinos baseado em Especificações Formais. A linguagem de especificação formal escolhida foi CSP-OZ, uma combinação de CSP e Object-Z. Object-Z é uma extensão orientada a objetos da linguagem Z para a especificação de predicados, tipicamente pré e pós condições, além de invariantes de dados. CSP (Communicating Sequential Process) é uma álgebra de processos desenvolvida para descrever modelos comportamentais de processos paralelos. A checagem de modelos especificados formalmente consiste na análise das especificações para verificar se um sistema possui certas propriedades através de uma busca exaustiva em todos os estados em que este pode entrar durante sua execução. Neste contexto, é possível checar corretude, livelocks, deadlocks, etc. Além disso, pode-se relacionar duas especificações diferentes a fim de se checar relações de refinamento. Para as especificações, o verificador de modelos FDR da Formal Systems Ltd. será utilizado. A implementação é desenvolvida utilizando um perfil da linguagem Ada denominado RavenSPARK, uma junção do perfil Ravenscar (desenvolvido na Universidade de York) com a linguagem SPARK (um subconjunto da linguagem Ada desenvolvido pela Praxis, Inc.). O Ravenscar é um perfil para desenvolvimento de processos, e portanto os processos de CSP, incluindo seus canais de comunicação, podem ser facilmente criados. Por outro lado, SPARK é uma linguagem onde podem ser inseridos predicados para os dados (originalmente especificados em Object-Z) utilizando anotações da própria linguagem. A linguagem SPARK possui uma ferramenta, o Examinador, que pode checar códigos de modelos baseado nestas anotações. Em resumo, o método proposto permite tanto a checagem de modelos em CSP quanto a checagem no nível de código. Para isso, as especificações em Object-Z devem inicialmente ser convertidas em um código na linguagem SPARK juntamente com suas respectivas anotações, para que então a checagem do modelo possa ser realizada no código. O desenvolvimento de uma arquitetura de controle reativa para um ROV denominado VSOR (Veículo Submarino Operado Remotamente) é utilizado como exemplo de uso do método proposto. Toda a arquitetura de controle é codificada utilizando a linguagem Ada com o perfil RavenSPARK e embarcada em um computador do tipo PC104 com o sistema operacional de tempo real VxWorks, da Windriver, Inc. / The development of control architectures for Underwater Vehicles is a complex task. These control architectures might be chracterised by the following attributes: real-time, multitasking, concurrency, and distributed over communication networks. In this scenario, we have multiple processes running in parallel, possibly distributed, and engaging in communication between each other. In this context, the behavioural model might lead to phenomena like deadlocks, livelocks, race conditions, among others. In order to try to minimize the effects of such difficulties, in this work a method for model checking control architectures of underwater vehicles based on formal specifications is presented. The chosen formal specification language is CSP-OZ, a combination of CSP and Object-Z. Object-Z is an object-oriented extension of Z for the specification of predicates, typically, data pre, post and invariant conditions. CSP (Communicating Sequential Process) is a process algebra developed to describe behavioural models of parallel process. The model checking of formal specifications is a task of reasoning on specifications in which a system verifies certain properties by means of an exhaustive search of all possible states that a system could enter during its execution. In this context, it is possible to check about correctness, liveness, deadlock, etc. Also, one can relate two different specifications in order to check a refinement ordering. For the specifications, the model checker FDR of Formal Systems Ltd. is utilised. The implementation is developed using an ADA language profile called RavenSPARK, a union of the Ravenscar profile (developed at the University of York) and the SPARK language (a subset of the ADA language developed by Praxis, Inc.). The Ravenscar is a profile for developing processes, so CSP processes including their message channels can be easily deployed. On the other hand, SPARK is a language where one can insert data predicates (originally specified in Object-Z) using language annotations. The SPARK language has a tool, the Examiner, that can model check code based on these annotations. In summary, the proposed method allows model checking of CSP processes but does not allow any checking in the code level. On the contrary, Object-Z specifications must first be converted into a SPARK language code, together with proper annotations, and then model checking can be realised in code. The development of a real-time reactive control architecture of an ROV named VSOR (Veiculo Submarino Operado Remotamente) is used as an example of the use of the proposed method. The whole control architecture is coded using the ADA Language with the RavenSPARK profile and deployed into a PC104 cpu system running the Vxworks real-time operating system of Windriver, Inc.

Estuda-se o problema de sintonia de controladores, objetivando-se a formulação do problema de sintonia ótima de controladores. Busca-se uma formulação que seja geral, ou seja, válida para qualquer estrutura de controlador e qualquer conjunto de especificações. São abordados dois temas principais: especificação de controladores e sintonia ótima de controladores. São compiladas as principais formas de especificação e avaliação de controladores e é feita a formulação do problema de sintonia de controladores como um problema padrão de otimização. A abordagem proposta e os conceitos apresentados são então aplicados em um conjunto de exemplos. / The problem of control tuning is studied, aiming the formulation of the optimal control tuning problem. A general formulation, valid for any controller structure and any set of specifications, is sought. Two main themes are addressed: controller specification and optimal controller tuning. The main ways of controller specification and assessment are compiled and the optimal controller tuning problem is formulated as a standard optimization problem. The proposed approach and the presented concepts are then applied in a set of examples.

Submitted by Israel Vieira Neto (israel.vieiraneto@ufpe.br) on 2015-03-06T14:22:22Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) DISSERTAÇÃO GIUSEPPE TREVISAN.pdf: 3587579 bytes, checksum: fa47c846ce99688bf17f94c5df29eb87 (MD5) / Made available in DSpace on 2015-03-06T14:22:22Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) DISSERTAÇÃO GIUSEPPE TREVISAN.pdf: 3587579 bytes, checksum: fa47c846ce99688bf17f94c5df29eb87 (MD5) Previous issue date: 2013-03-08 / FACEPE / Um segmento importante da literatura de Economia do Crime afirma que, além das variáveis socioeconômicas, o espaço é fator fundamental a se associar com a criminalidade. Dada a falta de evidências empíricas sobre a relação entre espaço e crime, este estudo tem por objetivo identificar as correlações entre as variáveis ambientais com a taxa de homicídio nos bairros da cidade do Recife. Para isso, foram construídas variáveis de ambiente que capturam características relacionadas à distribuição dos tipos de domicílios dos bairros do Recife e foi implementada a técnica de econometria espacial para averiguar efeitos de spillover espaciais. O modelo SAR apresenta o melhor ajuste e mostra que a proporção de estabelecimentos nãoresidenciais em relação ao total de estabelecimentos do bairro tem uma relação positiva com a criminalidade e a concentração de domicílios residenciais está associada a índices de criminalidades mais baixos. As correlações das variáveis socioeconômicas seguem o padrão da maioria dos achados da literatura nacional e internacional, exceto para o caso da densidade demográfica.

Submitted by João Arthur Martins (joao.arthur@ufpe.br) on 2015-03-11T19:12:53Z No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Approved for entry into archive by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-03-13T13:12:01Z (GMT) No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-13T13:12:01Z (GMT). No. of bitstreams: 2 Dissertacao Marcelo de Andrade.pdf: 1169415 bytes, checksum: bbbc84fb17de4321f5fc8b9f6d9cdb6e (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2013-08-23 / Requisitos são um dos principais artefatos no desenvolvimento de um sistema. Para sistemas críticos, os requisitos são artefatos obrigatórios para satisfazer critérios de certificações tais como os descritos no guia de certificação DO-178B. Apesar de sua importância, estes artefatos são geralmente descritos informalmente através de linguagem natural. O uso da linguagem natural propicia a descrição de requisitos ambíguos, incompletos e inconsistentes. Para sanar este problema foi definido o método Software Cost Reduction (SCR), que permite a descrição formal de requisitos de forma precisa e relativamente amigável através do uso de tabelas preenchidas com expressões lógicas. Em particular, de forma a nos aproximarmos ainda mais das tecnologias usadas na indústria de sistemas críticos, neste trabalho nosso SCR é o implementado na ferramenta TTM da suíte T-VEC (um conjunto de ferramentas que suporta a sintaxe de SCR e possibilita a geração de vetores de testes e análise de propriedades), a qual é capaz de gerar casos de teste seguindo o guia DO-178B. Além dos requisitos, a certificação do código implementado também é uma obrigação para sistemas críticos e o uso de SCR somente não garante isso. Enquanto o método SCR auxilia na descrição detalhada de requisitos, o ambiente de desenvolvimento baseado em modelos denominado Safety Critical Application Development Environment (SCADE) auxilia na modelagem de software crítico. SCADE é também usado para gerar código certificado de acordo com o DO-178B. Neste trabalho apresentamos como obter modelos SCADE a partir de especificações descritas em SCR através da aplicação de regras de tradução. Com isto obtemos código certificado a partir de requisitos formais em uma única solução. Para aplicar as regras de forma automática, construímos uma ferramenta tradutora usando o framework Stratego/ XT. Por fim, aplicamos nosso tradutor em dois estudos de caso descritos em SCR. Foi feito uso de uma estratégia de verificação baseada em testes para atestar que os modelos SCADE produzidos por nosso tradutor correspondem às descrições em SCR. A estratégia de verificação consiste em usar T-VEC para gerar vetores de testes de acordo com o critério de cobertura MCDC e então aplicar os testes no código C gerado pelo SCADE. Apesar de nosso tradutor não ser provado correto, podemos argumentar indiretamente que o mesmo preserva as propriedades descritas em SCR nos modelos SCADE gerados automaticamente. Quanto a certificação do tradutor, isto fica a cargo de nosso parceiro industrial Embraer S.A. .