Made available in DSpace on 2016-08-29T15:33:23Z (GMT). No. of bitstreams: 1 tese_9288_Ata de Defesa.pdf: 225566 bytes, checksum: 6da0bfa73a8135bc0ede55dc01438148 (MD5) Previous issue date: 2015-10-30 / CAPES / A modelagem de situações para aplicações sensíveis ao contexto, também chamadas de aplicações sensíveis a situações, é, por um lado, uma tarefa chave para o funcionamento adequado dessas aplicações. Por outro lado, essa também é uma tafera árdua graças à complexidade e à vasta gama de tipos de situações possíveis. Com o intuito de facilitar a representação desses tipos de situações em tempo de projeto, foi criada a Linguagem de Modelagem de Situações (Situation Modeling Language - SML), a qual se baseia parcialmente em ricas teorias ontológicas de modelagem conceitual, além de fornecer uma plataforma de detecção de situação em tempo de execução. Apesar do benefício da existência dessa infraestrutura, a tarefa de definir tipos de situação é ainda não-trivial, podendo carregar problemas que dificilmente são detectados por modeladores via inspeções manuais. Esta dissertação tem o propósito de melhorar e facilitar ainda mais a definição de tipos de situação em SML propondo: (i) uma maior integração da linguagem com as teorias ontológicas de modelagem conceitual pelo uso da linguagem OntoUML, visando aumentar a expressividade dos modelos de situação; e (ii) uma abordagem para validação de tipos de situação usando um método formal, visando garantir que os modelos criados correspondam à intenção do modelador. Tanto a integração quanto a validação são implementadas em uma ferramenta para especificação, verificação e validação de tipos de situação ontologicamente enriquecidos. / The modeling of situation types for context-aware applications, also called situationaware applications, is, on the one hand, a key task to the proper functioning of those applications. On the other hand, it is also a hard task given the complexity and the wide range of possible situation types. Aiming at facilitating the representation of those types of situations at design-time, the Situation Modeling Language (SML) was created. This language is based partially on rich ontological theories of conceptual modeling and is accompanied by a platform for situation-detection at runtime. Despite the benefits of the availability of this suitable infrastructure, the definition of situation types, being a non-trivial task, can still pose problems that are hardly detected by modelers by manual model inspection. This thesis aims at improving and facilitating the definition of situation types in SML by proposing: (i) the integration between the language and the ontological theories of conceptual modeling by using the OntoUML language, with the purpose of increasing the expressivity of situation type models; and (ii) an approach for the validation of situation type models using a lightweight formal method, aiming at increasing the correspondence between the created models’ instances and the modeler’s intentions. Both the integration and the validation are implemented in a tool for specification, verification and validation of ontologically-enriched situation types.

Atualmente, com o apoio das aplicações de software, as empresas asseguram maior eficiência, agilidade e melhor tomada de decisão nos seus processos de negócio. Neste cenário altamente competitivo, frequentemente surgem novas necessidades de negócio, o que leva as empresas a evoluir ou criar novos processos. Adicionar novas funcionalidades ao ecossistema de software da empresa, a partir da reutilização das aplicações existentes, não é uma tarefa trivial e exige metodologias, técnicas e ferramentas adequadas para construir soluções de integração. O ecossistema de software das empresas é heterogêneo, pois geralmente suas aplicações são adquiridas de empresas terceirizadas e são desenvolvidas utilizando diferentes plataformas de desenvolvimento, o que dificulta a integração entre as aplicações, pois geralmente elas são desenvolvidas sem a preocupação da integração. A área de Integração de Aplicações Empresariais trata da integração das aplicações existentes no ecossistema de software das empresas por meio de uma solução de integração. Uma solução de integração pode ser representada por um modelo conceitual, que representa o processo de integração entre aplicações em alto nível de abstração. O Guaraná DSL é uma das tecnologias que possibilita projetar modelos conceituais de soluções de integração, utilizando uma sintaxe concreta gráfica e intuitiva. No entanto, a integração de aplicações não é uma tarefa trivial e o desenvolvimento da solução envolve além de custos, riscos como bugs e gargalos de performance que geralmente são observados após a implementação. Esta dissertação propõe analisar o comportamento e identificar gargalos de performance de uma solução de integração ainda na fase de projeto. Propõe-se o desenvolvimento de um modelo matemático de simulação equivalente ao modelo conceitual da solução, utilizando como base as Redes de Petri. O modelo de simulação foi verificado por meio de técnicas de verificação validadas na literatura. A principal contribuição deste trabalho foi a constatação de que é possível representar modelos conceituais de soluções de integração de aplicações por meio das Redes de Petri Estocásticas. O experimento realizado possibilitou identificar pontos de formação de filas, possíveis gargalos de desempenho e identificar comportamentos da solução de integração ainda na fase de projeto. / 99 f.

Made available in DSpace on 2016-06-02T19:05:51Z (GMT). No. of bitstreams: 1 3754.pdf: 2613907 bytes, checksum: fe0e2ffcc47c79299e0f1f18103dba89 (MD5) Previous issue date: 2011-02-25 / Around 37% of unsuccessfully software projects have their cause related to issues on how to software requirements are collected and manipulated. Requirement Management activities help on getting this scenario better, however it is necessary to validate the software under construction on its right meaning frequently. Thus, Software Quality Assurance (SQA) activities are very important to find defects on softwares under development, even before having an executable product version. The main SQA activities are Test and Inspection and, in spite of Test activity generally occurs during coding phase, this activity may and should be applied as soon as possible, as it needs planning to achieve its goal. Besides, many important Test Cases and Scenarios are specified once software development starts, during requirement specification and modeling phases. Thus, considering this scenario and also that Use Case Model is one of the most used techniques of requirement modeling, this work has the objective of implementing a module to generate Test Scenarios based on Use Cases. The module is a new added functionality to COCAR environment, which supports other software development activities based on use case model. This new module helps on Test activity automation, generating unity testing scenarios, related to each use case, and integration testing scenarios, that use the relationships among use cases, based on their specifications. The work evaluation was done based on real developed software, comparing the used test cases with the test scenarios generated by COCAR environment. The results have shown that the generated test scenarios have almost all of the used test cases matching. Thus, they can be used to support test plan and test cases definition. / Cerca de 37% dos casos de insucesso em projetos de software têm sua causa relacionada a problemas com a coleta e manipulação dos requisitos do software. Atividades de Gerência de Requisitos ajudam a melhorar esse quadro, mas é preciso validar constantemente o software sendo produzido quanto à sua fidelidade aos requisitos. Nesse sentido, as atividades de Garantia de Qualidade de Software (GQS) são muito importantes para encontrar defeitos no software sendo desenvolvido, antes mesmo que haja uma versão executável do produto. As principais atividades de GQS são Teste e Inspeção e, apesar do Teste se aplicar, geralmente, quando se está na fase de codificação, essa atividade pode e deve se iniciar o quanto antes, pois ela precisa de planejamento para ser bem sucedida. Além disso, muitos dos Cenários e Casos de Teste relevantes são determinados logo no início do desenvolvimento, ainda em fase de levantamento e modelagem dos requisitos. Assim, considerando esse contexto e considerando também que uma das técnicas mais usadas para a modelagem dos requisitos é o Modelo de Casos de Uso, este trabalho teve por objetivo implementar um módulo para geração de Cenários de Teste a partir de Casos de Uso. Esse módulo corresponde a uma funcionalidade adicional no ambiente COCAR, o qual apóia outras atividades do desenvolvimento de software com base nos modelos de casos de uso. O módulo implementado no ambiente contribuiu para a automatização da atividade de Teste com a geração de cenários de teste unitários, que se referem aos casos de uso individualmente, e cenários de teste de integração, que exercitam as relações de dependência existentes entre os casos de uso de um sistema, sempre com base em suas especificações. A avaliação do trabalho foi feita com base em um sistema real que já estava desenvolvido e para o qual foram comparados os cenários de teste usados quando ele foi desenvolvido e os cenários gerados pelo ambiente COCAR. Os resultados mostraram que os cenários gerados contemplam quase que totalmente os cenários definidos manualmente e, portanto, podem ser usados como suporte à definição do plano de teste e aos casos de teste.

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.

A transferência de odores entre os gatos e o meio ambiente ocorre por meio de contatos corporais, como também pela eliminação de excretas. Pelo enriquecimento ambiental é possível promover a exibição de comportamentos mais próximos dos naturais e extinguir comportamentos não desejáveis, contribuindo, assim, para a saúde física e psicológica dos animais. Este trabalho teve como objetivo promover estímulos no ambiente para que os gatos desempenhassem comportamentos característicos da espécie. Foram utilizados gatos domésticos (Felis silvestris catus L.), castrados (por volta do primeiro ano de vida) ou não, de ambos os sexos. Os animais foram mantidos todos juntos em um abrigo de gatos, cuja população era de aproximadamente 110 indivíduos, sendo 41 machos e 69 fêmeas. Cinco testes foram realizados durante dezesseis meses e foi registrado: quais os comportamentos são manifestados na área dos testes (grooming, urinar, defecar e verificações olfativas), quais indivíduos realizaram mais esses comportamentos (fêmeas, machos e machos castrados) e qual categoria animal apresentou maior número de contato. Foram utilizados o método animal focal e a amostragem do comportamento. Observou-se que existe diferença significativa nos contatos entre machos e fêmeas (Fr= 10, 362, p= 0, 006) e averiguou-se que essa diferença também ocorre quando os grupos são agregados (contatos F_M-M_M e contatos F_F-F_M). Fêmeas e machos castrados, quando comparados pelo teste Wilcoxon, apresentaram diferenças significativas no tempo dedicado ao comportamento de grooming(z= 2,95, p= 0,036). Os gatos são indivíduos bastante curiosos, o que facilita o desenvolvimento de um enriquecimento ambiental mais barato com o alcance de respostas comportamentais adequadas. / The transfer of odors between the cats and the environment occurs through physical contact, but also for disposal of excreta. For environmental enrichment can promote behaviors closer view of the natural and extinguish unwanted behaviors, thus contributing to the physical and psychological health of animals. This work aimed to promote the environment for stimuli that cats play behaviors characteristic of the species. We used domestic cats (Felis silvestris catus L.), castrated (around the first year of life) or not, of both sexes. The animals were kept together in a shelter for cats, whose population was approximately 110 individuals, 41 males and 69 females. Five tests were conducted over sixteen months and was recorded: which behaviors are manifested in the area of testing (grooming, urinate, defecate and verification olfactory), which made most people these behaviors (females, males and castrated males) and which category of animal presented more contact. We used the method of sampling and focal animal behavior. It was observed that there is significant difference in contacts between males and females (F = 10, 362, p = 0, 006) and checked that this difference also occurs when the groups are aggregated (F_M contacts and contacts F_F-M_M-F_M ). Females and castrated males, when compared by Wilcoxon test showed significant differences in time devoted to grooming behavior of (z = 2.95, p = 0.036). Cats are very curious people, which facilitates the development of an environmental enrichment cheaper with the range of appropriate behavioral responses.

Planejamento sob incerteza vem sendo cada vez mais requisitado em aplicações práticas de diversas áreas que eequerem soluções confiáveis para metas complexas. Em vista disso, nos últimos anos, algumas abordagens baseadas no uso de métodos formais para síntese automática de planos têm sido propostas na área de Planejamento em Inteligência Artificial. Entre essas abordagens, planejamento baseado em verificação de modelos tem se mostrado uma opção bastante promissora; entretanto, conforme observamos, a maioria dos trabalhos dentro dessa abordagem baseia-se em CTL e trata apenas problemas de planejamento para metas de alcançabilidade simples (como aquelas consideradas no planejamento clássico). Nessa tese, introduzimos uma classe de metas de planejamento mais expressivas (metas de alcançabilidade estendidas) e mostramos que, para essa classe de metas, a semântica de CTL não é adequada para formalizar algoritmos de síntese (ou validação) de planos. Como forma de contornar essa limitação, propomos uma nova versão de CTL, que denominamos alpha-CTL. Então, a partir da semântica dessa nova lógica, implementamos um verificador de modelos (Vactl), com base no qual implementamos também um planejador (Pactl) capaz de resolver problemas de planejamento para metas de alcançabilidade estendidas, em ambientes não-determinísticos com observabilidade completa. Finalmente, discutimos como garantir a qualidade das soluções quando dispomos de um modelo de ambiente onde as probabilidades das transições causadas pela execução das ações são conhecidas. / Planning under uncertainty has being increasingly demanded for practical applications in several areas that require reliable solutions for complex goals. In sight of this, in the last few years, some approaches based on formal methods for automatic synthesis of plans have been proposed in the area of Planning in Artificial Intelligence. Among these approaches, planning based on model checking seems to be a very attractive one; however, as we observe, the majority of the works in this approach are mainly based on CTL and deals only with planning problems for simple reachability goals (as those considered in classical planning). In this thesis, we introduce a more expressive class of planning goals (extended reachability goals) and show that, for this class of goals, the CTL\'s semantics is not adequate to formalize algorithms for synthesis (or validation) of plans. As a way to overcome this limitation, we propose a new version of CTL, called alpha-CTL. Then, based on the semantics of this new logic, we implement a model checker (Vactl), based on which we also implement a planner (Pactl) capable of solving planning problems for extended reachability goals, in nondeterministic planning environments with complete observability. Finally, we discuss how to guarantee the quality of the solutions when we have an environment model where the actions transitions probabilities are known.

The increase of computer systems complexity has led to a direct increase in the difficulty of verifying their correctness. For mastering this complexity, formal methods can be used in the development of systems providing techniques for both design and verification. Regarding concurrent and distributed systems, the necessity of a formal approach is more prominent given the substantial increase in complexity due to the countless number of interactions between their constituent systems. Unfortunately, however, current methods are not capable of dealing with the automated analysis of such systems in general, even if we consider only classical properties such as deadlock freedom; the state explosion problem is the main reason for this ineffectiveness. This work is a contribution in this direction. Particularly, considering networks of CSP processes, this work proposes a local strategy for deadlock analysis based on the notion of process refinement. The locality of this strategy prevents the state explosion problem generated by the interaction of constituent systems, which represents a major asset of our strategy. We define a refinement assertion for checking conflict freedom between pairs of processes in the network; this can be used for the local verification of networks with an acyclic communication topology. Concerning networks with a cyclic communication topology, we propose three patterns that prevent deadlocks: the resource allocation, the client/server and the async dynamic. These patterns impose behavioural and structural restrictions to prevent deadlocks. The behavioural restrictions are also captured by refinement assertions, which enable one to automatically verify these conditions using a refinement checker. Besides this, we develop four case studies to evaluate the efficiency of our strategy in practice: a ring buffer, a dining philosopher, and two variations of a leadership election algorithm. One of the variations of the leadership election algorithm consists of a model used in practice by the B&O Company, an industrial partner. In this study, we compare our strategy with two other techniques for deadlock freedom verification, the SSD algorithm of the Deadlock Checker tool and the built-in deadlock freedom assertion of FDR. This study demonstrates how our strategy can be used and that it might be a useful alternative to analysing complex industrial systems for deadlock freedom. / Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-10T16:54:41Z No. of bitstreams: 2 DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-11T17:34:41Z (GMT). No. of bitstreams: 2 DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2014-03-31 / Com o aumento da complexidade dos sistemas computacionais, houve também um aumento da dificuldade na tarefa de verificação de sistemas. Para lidar com essa complexidade, métodos formais podem ser usados no desenvolvimento de sistemas, fornecendo técnicas para a modelagem e verificação. No contexto de sistemas concorrentes e distribuídos, a necessidade de uma abordagem formal é ainda mais proeminente, dadas as inúmeras possibilidades de interação entre seus sistemas componentes. Entretanto, infelizmente, os métodos atuais não se encontram, de forma geral, completamente aptos a lidar com a análise automática desses sistemas, mesmo em se tratando de propriedades clássicas como a ausência de deadlocks. A explosão do espaço de estados a ser analisado é o principal fator para essa ineficácia por parte desses sistemas. O trabalho apresentado é uma contribuição nesta direção. Considerando o conceito de redes de processos CSP, o presente trabalho propõe uma estratégia local para a análise de deadlocks baseada na noção de refinamento de processos. A localidade dessa estratégia previne a explosão de espaço de estados causada pela interação de sistemas componentes, o que constitui uma vantajosa característica da nossa estratégia. O trabalho define uma expressão de refinamento capturando o conceito de ausência de conflito, que pode ser usado para verificar localmente que uma rede de processos com uma topologia de comunicação acíclica é livre de deadlocks. Para as redes com topologia cíclica, o trabalho sistematiza e formaliza três padrões comportamentais que impedem deadlocks: o alocação de recursos, o cliente/servidor e o assíncrono dinâmico. Esses padrões impõem restrições comportamentais e estruturais para prevenir deadlocks. Essas restrições comportamentais também são capturadas através de expressões de refinamento, o que possibilita a verificação automática dessas condições com o uso de um verificador de refinamento. Além disso, são apresentados quatro estudos de caso usados para avaliar o desempenho da nossa técnica na prática: um buffer circular, um jantar dos filósofos e duas variações de um algoritmo para eleição de líder. Uma dessas variações consiste num modelo usado na prática pela empresa B&O, um parceiro industrial. Nesse estudo, avaliamos a nossa técnica em comparação com outras duas técnicas para verificação de ausência de deadlocks, o algoritmo SSD da ferramenta Deadlock Checker e a asserção de verificação de deadlocks padrão do verificador de modelos FDR. Esse estudo demonstra como a nossa estratégia é aplicada e que ela pode ser uma alternativa vantajosa para a verificação de sistemas complexos.

Submitted by Daniella Sodre (daniella.sodre@ufpe.br) on 2015-04-17T13:23:49Z No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) TESE Tiago Figueiredo Vieira.compressed.pdf: 2116364 bytes, checksum: b3851944ff7105bff9fdcd050d5d4f86 (MD5) / Made available in DSpace on 2015-04-17T13:23:49Z (GMT). No. of bitstreams: 2 license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) TESE Tiago Figueiredo Vieira.compressed.pdf: 2116364 bytes, checksum: b3851944ff7105bff9fdcd050d5d4f86 (MD5) Previous issue date: 2013-11-08 / A investigação da face humana é comum em análise de padrões/ processamento de imagens. Abordagens tradicionais são a identificação e a verificação mas muitas outras estão surgindo, como estimativa de idade, análise de similaridade, atratividade e o reconhecimento de parentesco. Apesar deste último possuir diversas possíveis aplicações, poucos trabalhos foram apresentados até então. Esta tese apresenta um algoritmo apto a discriminar entre irmãos e não irmãos, baseado nas imagens das suas faces. Um grande desafio foi lidar com a falta de um benchmark em análise de parentesco e, por esta razão, uma base de imagens de alta qualidade de pares de irmãos foi coletada. Isto é uma contribuição relevante à comunidade científica e foi particularmente útil para evitar possíveis problemas devido a imagens de baixa qualidade e condições não-controladas de aquisição de bases de dados heterogêneas usadas em outros trabalhos. Baseado nessas imagens, vários classificadores foram construídos usando técnicas baseadas na extração de características e holística para investigar quais variáveis são mais eficientes para distinguir parentes. As características foram primeiramente testadas individualmente e então as informações mais significantes da face foram fornecidas a um algoritmo único. O classificador de irmãos superou a performance de humanos que avaliaram a mesma base de dados. Adicionalmente, a boa capacidade de distinção do algorimo foi testado aplicando-o a uma base de dados de baixa qualidade coletada da Internet. O conhecimento obtido da análise de irmãos levou ao desenvolvimento de um algoritmo similar capaz de distinguir pares pai-filho de indivíduos não relacionados. Os resultados obtidos possuem impactos na recuperação e anotação automática de bases de dados, ciência forense, pesquisa genealógica e na busca de familiares perdidos.----------------------------------------------------------------------------------------------- The investigation of human face images is ubiquitous in pattern analysis/ image processing research. Traditional approaches are related to face identification and verification but, several other areas are emerging, like age/ expression estimation, analysis of facial similarity and attractiveness and automatic kinship recognition. Despite the fact that the latter could have applications in fields such as image retrieval and annotation, little work in this area has been presented so far. This thesis presents an algorithm able to discriminate between siblings and unrelated individuals, based on their face images. In this context, a great challenge was to deal with the lack of a benchmark in kinship analysis, and for this reason, a high-quality dataset of images of siblings’ pairs was collected. This is a relevant contribution to the research community and is particularly useful to avoid potential problems due to low quality pictures and uncontrolled imaging conditions of heterogeneous datasets used in previous researches. The database includes frontal, profile, expressionless and smiling faces of siblings pairs. Based on these images, various classifiers were constructed using feature-based and holistic techniques to investigate which data are more effective for discriminating siblings from non-siblings. The features were first tested individually and then the most significant face data were supplied to a unique algorithm. The siblings classifier has been found to outperform human raters on all datasets. Also, the good discrimination capabilities of the algorithm is tested by applying the classifiers to a low quality database of images collected from the Internet in a cross-database experiment. The knowledge acquired from the analysis of siblings fostered a similar algorithm able to discriminating parent-child pairs from unrelated individuals. The results obtained in this thesis have impact in image retrieval and annotation, forensics, genealogical research and finding missing family members.

Made available in DSpace on 2014-06-12T15:56:13Z (GMT). No. of bitstreams: 2 arquivo2770_1.pdf: 3435334 bytes, checksum: c4ebc011cd6476e268421539acd59c8c (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2009 / Associação para Promoção da Excelência do Software Brasileiro / O gerenciamento e o projeto de sistemas de engenharia complexos é um desafio interessante. A engenharia de sistemas é um campo interdisciplinar da engenharia focado na melhoria da qualidade de projetos de sistemas. Ela encoraja o uso de métodos e ferramentas como simulação, otimização, análise de confiabilidade e análise estatística para aumentar o conhecimento do sistema, frequentemente representado como um conjunto de modelos. Uma enorme variedade de sistemas dinâmicos precisa ser controlada e pode ser modelada usando os princípios da Teoria de Controle, a base da disciplina de engenharia de controle. Em particular, a engenharia de controle objetiva criar leis de controle para o sistema, que são modeladas usando diagramas de bloco (também chamados de diagramas de leis de controle) e validadas/verificadas usando simulação. Entretanto, a maior parte das validações de leis de controle realizadas na indústria é feita usando ferramentas de simulação como o Simulink, e simulações não cobrem todos os comportamentos do modelo. Além disso, não é fácil modelar uma arquitetura complexa na qual redundância e monitoramento são comumente usados para se obter segurança. Neste trabalho, nós apresentamos três principais contribuições: (1) um conjunto de regras de tradução de modelos Simulink para a algebra de processos CSP (Communicating Sequential Processes), incluindo uma infraestrutura para suportar vários blocos discretos de Simulink; (2) uma estratégia para validar a integração de uma proposta de arquitetura com as leis de controle; e (3) a validação de um sistema de controle de voo dos profundores de um avião produzido pela Embraer. Os resultados mostram que a estratégia pode ser aplicada a modelos complexos através do uso das técnicas formais de abstração de dados e verificação de modelos. Ademais, a estratégia proposta aprimora o processo de desenvolvimento padrão (modelo V) seguido pela indústria por encontrar potenciais defeitos em fases de especificação do projeto, reduzindo tempo de desenvolvimento e custos

Made available in DSpace on 2014-06-12T15:56:15Z (GMT). No. of bitstreams: 2 arquivo2793_1.pdf: 1387248 bytes, checksum: e99d52780679d746f07f5ff17549301a (MD5) license.txt: 1748 bytes, checksum: 8a4605be74aa9ea9d79846c1fba20a33 (MD5) Previous issue date: 2010 / É crescente a necessidade de controle de acesso a lugares, serviços e informações. É crescente também a busca por soluções mais eficientes na identificação pessoal. Neste contexto, a biometria, que consiste no uso de características biológicas como mecanismo de identificação, tem sido utilizada com resultados bastante promissores. Dentre as informações utilizadas para identificação dos indivíduos podem ser destacadas a íris, a retina, a face, a impressão digital ou até mesmo a geometria da mão. Dentre as biometrias, o reconhecimento de faces destaca-se por ser uma técnica que apresenta ótimos resultados com baixo custo de implantação. Ela pode ser utilizada nos mais diversos tipos de dispositivos e, em sua forma mais simples, não exige hardware dedicado. A técnica destaca-se ainda por não necessitar da interação do usuário ou qualquer tipo de contato físico para captura e classificação das faces. O presente trabalho é focado no reconhecimento de faces baseado em imagens (2D). Mais precisamente o trabalho visa reduzir ou eliminar os efeitos de variações no ambiente ou na própria face que prejudiquem a sua classificação final. As técnicas examinadas e propostas fazem uso da análise de componentes principais (PCA) para extração de características das imagens de faces frontais. Elas baseiam-se em estudos recentes com o objetivo de melhorar as taxas de classificação mesmo sob condições adversas de aquisição de imagens ou oclusão parcial das faces. Os resultados obtidos mostraram uma superioridade nas taxas de acerto das abordagens propostas em relação às suas técnicas-base quando executadas sobre imagens com algum tipo de variação local. Foi constatado também um grande ganho no tempo de processamento das imagens, o que contribui para aplicar as técnicas propostas em dispositivos com menor capacidade computacional