Made available in DSpace on 2014-06-12T15:08:12Z (GMT). No. of bitstreams: 2 arquivo270_1.pdf: 1826236 bytes, checksum: f1bee41d5be9c17c7474287e0bf3c9ae (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2010 / A atmosfera de loja foi proposta por Kotler (1973) como uma ferramenta de marketing que utiliza o planejamento consciente do espaço para obter determinadas respostas dos consumidores. No varejo de vestuário, o ambiente dos provadores de roupas é um dos espaços que pode compor a atmosfera de loja. A presente dissertação investigou como o ambiente dos provadores de roupas em lojas de vestuário se relaciona com os estágios de avaliação e decisão de compra do consumidor. O estudo possui uma abordagem qualitativa, realizando-se para a coleta de dados uma pesquisa de campo com a utilização de entrevistas com consumidores e vendedores, observação direta em ambientes de provadores e observação indireta por meio de fotografias. Na análise do material coletado foram usados os métodos de foto-documentação e de análise de conteúdo. Os principais resultados indicam que, em relação aos fatores sensoriais do ambiente, espaços pequenos e quentes podem diminuir o tempo de permanência no local, a iluminação indireta é preferida pelos consumidores e a ausência de espelhos, bancos ou prendedores de roupas pode irritar os clientes. No tocante aos aspectos sociais, a privacidade é um elemento importante e a opinião de familiares, amigos e vendedores podem influenciar na decisão de consumo, já em relação a divergências entre homens e mulheres, poucas diferenças foram encontradas e, ambos, podem ser influenciados por estímulos presentes no ambiente dos provadores

Made available in DSpace on 2014-06-11T19:29:32Z (GMT). No. of bitstreams: 0 Previous issue date: 2006-01-30Bitstream added on 2014-06-13T19:59:13Z : No. of bitstreams: 1 macatelli_m_me_arafcf.pdf: 832166 bytes, checksum: 9d5940654a5922cf9983e1c2b1c0b6a8 (MD5) / Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP) / Universidade Estadual Paulista (UNESP) / A cachaça é o destilado mais consumido no Brasil e ocupa o segundo lugar entre as bebidas alcoólicas, perdendo somente para a cerveja. O consumo brasileiro lhe garante a terceira colocação entre os destilados do mundo inteiro, atrás somente da vodca e do soju (ABRABE, 2004). Neste estudo, através da Análise Descritiva Quantitativa (ADQ), 10 amostras de cachaça, envelhecidas e não envelhecidas, de diferentes regiões do país e importantes no mercado interno e externo, foram avaliadas sensorialmente por uma equipe de 10 provadores treinados e selecionados, inicialmente inexperiente com técnicas de análise sensorial. Desenvolveu-se o perfil sensorial das amostras, levantando-se 12 atributos relacionados à caracterização e diferenciação da bebida, ressaltando-se ainda o efeito do envelhecimento no estabelecimento de características marcantes da cachaça e melhorando sua qualidade sensorial. Técnicas estatísticas não tradicionalmente empregadas na ADQ, como a Análise Procrustes Generalizada e correlações, revelaram-se como boas opções para explorar os dados e validar os resultados da análise quando se utiliza equipes inexperientes e produtos de difícil avaliação / Cachaça is the distilled beverage more consumed in Brazil. Considering all the alcoholic drinks, cachaça is the second one in the rank, just after the beer level. This intense internal consumption of the Brazilian spirit had positioned the cachaça as the third one between all distillates in the world, just after vodka and soju (ABRABE, 2005). In this study, quantitative descriptive analysis (QDA) was used to evaluate 10 cachaça samples, matured in wood and immature ones, from different regions of the country and important to the internal and external market. The sensory evaluation used a panel composed by 10 assessors, initially inexperienced in sensory analysis techniques. The sensory profiles of the samples were developed, including 12 attributes related to cachaça characterization and differentiation. The effect of the maturation process on the beverage character and sensory quality were also highlighted. Non traditional statistics techniques, like Generalized Procrustes Analysis and correlations, were also used in the QDA. The new methods were considered as good options to explore data and validate results, especially when inexperienced panel is used and difficult products are analyzed.

Submitted by Alice Araujo (alice.caraujo@ufpe.br) on 2017-11-29T17:56:29Z No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) dissertação_vanessa_larize_final.pdf: 1152292 bytes, checksum: 2bd44824bd4445f9e134fc21621a468a (MD5) / Made available in DSpace on 2017-11-29T17:56:29Z (GMT). No. of bitstreams: 2 license_rdf: 811 bytes, checksum: e39d27027a6cc9cb039ad269a5db8e34 (MD5) dissertação_vanessa_larize_final.pdf: 1152292 bytes, checksum: 2bd44824bd4445f9e134fc21621a468a (MD5) Previous issue date: 2016-09-15 / FACEPE / O uso de sistemas eletrônicos embarcados está cada vez mais presente no dia a dia da sociedade. Telefones celulares,sistemas de posicionamento global (GPS) e televisores digitais com telas de LCD são exemplos de equipamentos que estão incorporando funcionalidades para atender às demandas dos usuários, e, consequentemente, aumentando a complexidade dos sistemas embarcados nesses dispositivos. De fato, a grande maioria das inovações em sistemas embarcados é atribuída aos avanços na microeletrônica e no projeto de software embarcado. Porém, devido a atual complexidade dos dispositivos, projetos de hardware não conseguem acompanhar o crescimento da capacidade física do hardware, havendo um gap de produtividade entre o desenvolvimento do hardware e o desenvolvimento do software necessário para a sua operação. Esses softwares, também conhecidos como Software dependente do Hardware (Hardware-dependent Software - HdS ), estão no centro do desafio do projeto de sistemas. Dentre esses HdS, pode-se citar os device drivers ou drivers dos dispositivos. Os drivers são codificados com base na documentação disponível pelos fornecedores do hardware, porém, na maioria das vezes, esse documento não é de fácil leitura, podendo levar a erros de interpretação. Atrelado a isso, como essa documentação está escrita em uma linguagem natural, a descrição do dispositivo pode ser muitas vezes ambígua, incompleta, ou até mesmo inconsistente. Além desses problemas, o device driver tem acesso a vários recursos do sistema operacional, assim qualquer erro nesta camada de software pode ser fatal. Por isso, essa camada de software deve ser cuidadosamente desenvolvida e testada. Com o intuito de reduzir os erros nos devices drivers, em MACIEIRA; BARROS; ASCENDINA (2014) foi proposta uma técnica de formalização e validação em tempo de execução de propriedades temporais e protocolos de comunicação de alto nível entre os dispositivos e seus devices drivers utilizando a linguagem TDevC. Mas, na especificação do trabalho anterior, a máquina de estados hierárquica gerada ainda pode conter estados não-determinísticos e propriedades temporais contraditórias. Dessa forma, o presente trabalho propõe uma técnica para validação de uma especificação TDevC para o desenvolvimento de device drivers robustos. Para isso, este trabalho faz uso do provador de teoremas de alto desempenho Z3 e das propriedades dos autômatos de Büchi. Para validação da proposta, foi utilizada a especificação TDevC do dispositivo Ethernet DM9000A.Nos experimentos realizados, verificou-se que o projeto conseguiu detectar as inconsistências na especificação TDevC em 100% dos casos. / The use of electronic embedded system has increased substantially. Mobile phones, Global Positioning System (GPS) and Digital television with LCD screens are examples of equipments that are incorporating features to meet the demands of users, and thereby increasing the complexity of embedded systems in these devices. In fact, the vast majority of innovations in embedded systems is attributed to advances in microelectronics and embedded software design. However, due to the current complexity of devices, hardware design cannot keep up the hardware capacity growth, with a productivity gap between the development of the hardware and the development of the software required for its operation. These softwares, also known as Hardware-dependent Software (HdS) are at the center of the design challenge systems. Among these HdS are the devices drivers. Drivers are encoded based on the documentation available by the hardware vendors, however, most of the time, this document is not easy to read and can lead to misinterpretations. Coupled to this, as this documentation is written in a natural language, the device description can often be ambiguous, incomplete or even inconsistent. In addition to these problems, the device driver has access to various operating system resources, so any error in this software layer can be fatal. Therefore, this software layer must be carefully developed and tested. In order to reduce errors in the device drivers, it has been proposed a technique for formalization and runtime validation of temporal properties in high-level communication protocols between devices and drivers using the TDevC language. But the hierarchical state machine, generate in the previous work, may contain nondeterministic states and contradictory temporal properties. Thus, this approach proposes a technique to validate a TDevC specification for the development of robust device drivers. Therefore, this work makes use of high-performance theorem prover Z3 and Buchi automata properties. Some experiments using the Ethernet device DM9000A TDevC specification showed that this approach is effective in detect TDevC specification inconsistency.

Dissertação (mestrado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, Mestrado em Informática, 2015. / Submitted by Albânia Cézar de Melo (albania@bce.unb.br) on 2015-03-31T15:40:32Z No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) / Approved for entry into archive by Ruthléa Nascimento(ruthleanascimento@bce.unb.br) on 2015-04-20T19:01:54Z (GMT) No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) / Made available in DSpace on 2015-04-20T19:01:54Z (GMT). No. of bitstreams: 1 2015_ThiagoCoelhoVieira.pdf: 662085 bytes, checksum: 8fae3df1c74c85937e5cd8c48823b60b (MD5) / Diversos tipos de lógicas são usadas como linguagens para descrever sistemas complexos e suas propriedades com a finalidade de serem verificadas formalmente. Provadores de teoremas baseados em tableaux são ferramentas computacionais capazes de realizar esta tarefa de verificação. Em (WDF98) é proposto um método de prova baseado em tableaux para duas lógicas epistêmico-temporais, KL(n) e BL(n). Neste trabalho implementamos o método de prova baseado em tableaux descrito em (WDF98) e apresentamos um algoritmo para verificação de propriedades epistêmicas e temporais sobre a estrutura do tableau construída por este método. / Logics are used as languages to describe complex systems and their properties in order to be formally verified. Tableaux-based theorem-provers are computational tools which can be used to perform this verification task. (WDF98) propose a proof method based on tableaux for both the epistemic-temporal logics KL(n) and BL(n) . In this work we implement the tableaux-based proof method described in (WDF98) and present an algorithm for verification of epistemic-temporal properties over the structure of the tableau built by this method.

Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.

[pt] Demonstrações em lógica podem tornar-se muito grandes e complexas. Para resolver problemas, e para estudar lógica, é comum valer-se de assistentes de demonstração. Um assistente de demonstração geral deve integrar ferramentas que ajudem a especificar as lógicas, as equações, os conjuntos de regras, e as estratégias de busca (semi) automática de demonstrações. A comunidade usuária de Provadores Automáticos de Teoremas conhece algumas ferramentas que atendem a estes requisitos. Entretanto, estas ferramentas não estão preparadas para lidar com demonstrações muito grandes. Trabalhos recentes sugerem que uma boa forma de chegar a demonstrações menores é usar grafos, ao invés de árvores, para representar demonstrações. Esta dissertação descreve e implementa uma máquina virtual baseada em grafo e um compilador para a confecção de provadores de teoremas baseados em grafo. Para validar a ferramenta, alguns estudos de casos e provadores de teoremas baseados em grafo são apresentados. / [en] Proofs in logic can become very big and complex. For problem solving, and to teach logic, it is common the use of proof assistants. A general proof assistant should integrate tools to help users on specifying the logics, the formulas, the sets of rules, and the very strategy to perform (semi) automatic proof search. The Automatic Theorem Provers community is aware of some tools that were designed to fulfill these requirements. However, these tools do not take the (possibly) huge size of a proof. Recent works have pointed out that a good way to achieve shorter proofs is the use of graphs, instead of trees, to represent proofs. This dissertation describes and implements a graph-based virtual machine and a compiler for the production of graph-based theorem provers. Some case studies, standard as well as graph-based theorem prover, are illustrated in order to validate the tool.

Submitted by JÚLIO HEBER SILVA (julioheber@yahoo.com.br) on 2017-04-11T19:28:47Z No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Approved for entry into archive by Luciana Ferreira (lucgeral@gmail.com) on 2017-04-12T14:32:03Z (GMT) No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) / Made available in DSpace on 2017-04-12T14:32:03Z (GMT). No. of bitstreams: 2 Dissertação - Nayara de Souza Silva - 2017.pdf: 2066646 bytes, checksum: 95e09b89bf69fe61277b09ce9f1812a6 (MD5) license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Previous issue date: 2017-03-07 / Fundação de Amparo à Pesquisa do Estado de Goiás - FAPEG / The process of developing computer systems takes into account many stages, in which some are more necessary than others, depending on the purpose of the application. The implementation stage is always necessary, indisputably. Sometimes the requirements analysis and testing phases are neglected. And, generally, the part of formal verification correctness is intended for few applications. The use of model checkers has been exploited in the task of validating a behavioral specification in its appropriate level of abstraction, notably specifications validation of critical systems, especially when they involve the preservation of human life, when the existence of errors entails huge financial loss or when deals with information security. Therefore, it proposes to apply formal verification techniques in the validation of the vehicular safety system Avoiding Doored System, considered as critical, in order to verify if the implemented system faithfully meets the requirements for it proposed. For that, it was used as a tool to verify its correctness the Specification and Verification System - PVS, detailing and documenting all the steps employed in the process of specification and formal verification. K / O processo de desenvolvimento de sistemas computacionais leva em conta muitas etapas, nos quais umas são tidas mais necessárias que outras, dependendo da finalidade da aplica- ção. A etapa de implementação sempre é necessária, indiscutivelmente. Por vezes as fases de análise de requisitos e de testes são negligenciadas. E, geralmente, a parte de verifica- ção formal de corretude é destinada a poucas aplicações. O uso de verificadores de modelos tem sido explorado na tarefa de validar uma especificação comportamental no seu nível adequado de abstração, sobretudo, na validação de especificações de sistemas críticos, principalmente quando estes envolvem a preservação da vida humana, quando a existência de erros acarreta enorme prejuízo financeiro ou quando tratam com a segurança da informa- ção. Diante disso, se propõe aplicar técnicas de verificação formal na validação do sistema de segurança veicular Avoiding Doored System, tido como crítico, com o intuito de atestar se o sistema implementado atende, fielmente, os requisitos para ele propostos. Para tal, foi utilizada como ferramenta para a verificação de sua corretude o Specification and Verification System - PVS, detalhando e documentando todas as etapas empregadas no processo de especificação e verificação formal. Pal

Nesta tese apresentamos o projeto e a implementação do KEMS, um provador de teoremas multi-estratégia baseado no método de tablôs KE. Um provador de teoremas multi-estratégia é um provador de teoremas onde podemos variar as estratégias utilizadas sem modificar o núcleo da implementação. Além de multi-estratégia, o KEMS é capaz de provar teoremas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi. Listamos abaixo algumas das contribuições deste trabalho: * um sistema KE para mbC que é analítico, correto e completo; * um sistema KE para mCi que é correto e completo; * um provador de teoremas multi-estratégia com as seguintes características: - aceita problemas em três sistemas lógicos: lógica clássica proposicional, mbC e mCi; - tem seis estratégias implementadas para lógica clássica proposicional, duas para mbC e duas para mCi; - tem treze ordenadores que são usados em conjunto com as estratégias; - implementa regras simplificadoras para lógica clássica proposicional; - possui uma interface gráfica que permite a visualização de provas; - é de código aberto e está disponível na Internet em http://kems.iv.fapesp.br; * benchmarks obtidos através da comparação das estratégias para lógica clássica proposicional resolvendo várias famílias de problemas; - sete famílias de problemas para avaliar provadores de teoremas paraconsistentes; * os primeiros benchmarks para as famílias de problemas para avaliar provadores de teoremas paraconsistentes. / In this thesis we present the design and implementation of KEMS, a multi-strategy theorem prover based on the KE tableau inference system. A multi-strategy theorem prover is a theorem prover where we can vary the strategy without modifying the core of the implementation. Besides being multi-strategy, KEMS is capable of proving theorems in three logical systems: classical propositional logic, mbC and mCi. We list below some of the contributions of this work: * an analytic, correct and complete KE system for mbC; * a correct and complete KE system for mCi; * a multi-strategy prover with the following characteristics: - accepts problems in three logical systems: classical propositional logic, mbC and mCi; - has 6 implemented strategies for classical propositional logic, 2 for mbC and 2 for mCi; - has 13 sorters to be used alongside with the strategies; - implements simplification rules of classical propositional logic; - provides a proof viewer with a graphical user interface; - it is open source and available on the internet at http://kems.iv.fapesp.br; * benchmark results obtained by KEMS comparing its classical propositional logic strategies with several problem families; * seven problem families designed to evaluate provers for logics of formal inconsistency; * the first benchmark results for the problem families designed to evaluate provers for logics of formal inconsistency.

Made available in DSpace on 2014-12-17T15:48:07Z (GMT). No. of bitstreams: 1 AntonioAOVS.pdf: 849695 bytes, checksum: 575cdb368ae14f3aad606763ebea7114 (MD5) Previous issue date: 2004-10-13 / The widespread growth in the use of smart cards (by banks, transport services, and cell phones, etc) has brought an important fact that must be addressed: the need of tools that can be used to verify such cards, so to guarantee the correctness of their software. As the vast majority of cards that are being developed nowadays use the JavaCard technology as they software layer, the use of the Java Modeling Language (JML) to specify their programs appear as a natural solution. JML is a formal language tailored to Java. It has been inspired by methodologies from Larch and Eiffel, and has been widely adopted as the de facto language when dealing with specification of any Java related program. Various tools that make use of JML have already been developed, covering a wide range of functionalities, such as run time and static checking. But the tools existent so far for static checking are not fully automated, and, those that are, do not offer an adequate level of soundness and completeness. Our objective is to contribute to a series of techniques, that can be used to accomplish a fully automated and confident verification of JavaCard applets. In this work we present the first steps to this. With the use of a software platform comprised by Krakatoa, Why and haRVey, we developed a set of techniques to reduce the size of the theory necessary to verify the specifications. Such techniques have yielded very good results, with gains of almost 100% in all tested cases, and has proved as a valuable technique to be used, not only in this, but in most real world problems related to automatic verification / O grande crescimento do uso de smart cards (por bancos, companhias de transporte, celulares, etc) trouxe um fato importante, que deve ser considerado: a necessidade de ferramentas que possam ser usadas para verificar os cart?es, para que se possa garantir a corretude de seu software. Como a grande maioria dos cart?es desenvolvidos hoje em dia usa a tecnologia JavaCard em sua camada de software, o uso da Java Modeling Language (JML) para especificar os programas aparece como uma solu?ao natural. JML ? uma linguagem de especifica??o formal ligada ao Java. Ela foi inspirada pelas metodologias de Larch e Eiffel, e foi largamente adotada como a linguagem de facto em se tratando da especifica??o de qualquer programa relacionado ? Java. V?rias ferramentas que fazem uso de JML j? foram desenvolvidas, cobrindo uma grande gama de funcionalidades, entre elas, a verifica??o em tempo de execu??o e est?tica. Mas as ferramentas existentes at? o momento para a verifica??o est?tica n?o s?o totalmente automatizadas, e, aquelas que s?o, n?o oferecem um n?vel adequado de completude e seguran?a. Nosso objetivo ? contribuir com uma s?rie de t?cnicas, que podem ser usadas para alcan?ar uma verifica??o completamente autom?tica e segura para applets JavaCard. Nesse trabalho n?s apresentamos os primeiros passos nessa dire??o. Com o uso de uma plataforma de software composta pelo Krakatoa, Why e haRVey, n?s desenvolvemos um conjunto de t?cnicas para reduzir o tamanho da teoria necess?ria para verificar as especifica??es. Tais t?cnicas deram resultados muito bons, com ganhos de quase 100% em todos os testes que realizamos, e se provou como uma t?cnica que deve ser sempre considerAda, n?o somente nesse, mas na maioria dos problemas reais relacionado com verifica??o autom?tica