Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. / The objective of this work is to join the proccess of belief revision and model checking to evaluate project specifications looking for inconsistences, using the universal fragment of Computation Tree Logic (CTL), known as ACTL, and revise them generating changes suggestions in the specification. Our approach will translate the model (software specification) and the property to be revised to classical logic. Then we will apply a SAT solver to verify the generated formulas satsifability. From the SAT solver answer, we will create changes valid suggestions to the specification making the translation back from classical logic to the original model. To generate the changes suggestions, we proposed a framework based on heuristics where different approaches and decisions can be implemented, aiming a better application for each project scope. We implemented a basic heuristic as an example and used it to test the implementation to analise the proposed algorithm

O uso de aeronaves não tripuladas (VANTs) tem crescido substancialmente nos últimos anos, tanto no campo militar quanto no civil. Roadmaps preveem que em um futuro próximo essas aeronaves compartilhem o espaço aéreo com aeronaves convencionais, exigindo novas arquiteturas de sistemas embarcados que possam garantir uma operação coordenada e segura desses robôs. A maior parte das suas missões baseia-se fortemente em um conjunto de sensores transportados pela aeronave como parte da payload da missão. Contudo, não é trivial a integração de diferentes missões em diferentes aeronaves, visto que ainda não há uma padronização para a comunicação nesses robôs. Para possibilitar essa associação foi proposto neste trabalho a criação de um middleware. Para que se pudesse entender sobre a área de conhecimento dos VANTs realizou-se uma pesquisa sobre esses veículos e suas aplicações e então um protocolo chamado Smart Sensor Protocol (SSP) foi modelado, utilizando-se de técnicas formais para isso. O comportamento do protocolo está modelado com diagrama de estados, seguindo uma gramática escrita utilizando a forma BNF. Este modelo foi verificado com a ferramenta UPPAAL e sua implementação testada em placas Arduino. Os resultados dos testes mostraram que o modelo é viável para o ambiente de embarcados críticos visto que ele provê as funcionalidades necessárias neste cenário sem acrescentar um overhead na comunicação / UNMANNED Aerial Vehicles applications have grown substantially in recent years, both in military and civil fields. Roadmaps predict that in the near future these aircrafts will share the airspace with the conventional planes, requiring new architectures for embedded systems which may ensure a coordinated and safe operation. Most of its tasks are mainly based on a set of sensors carried by the aircraft as part of its payload. However, it is not trivial to integrate different missions in different aircraft plataforms, since there is no standardization for communication in such robots yet. To enable this type of association it was proposed in this masters project the designing of a middleware. It has been carried out a bibliographic review to find out the state-of-the-art in such field, including the specific applications in UAVs, and then a protocol has been modeled following formal techniques. This protocol is called Smart Sensor Protocol (SSP). The SSPs behavior was modeled through state diagrams according to a grammar described using BNF form. This model was verified with the UPPAAL tool and its implementation was run and tested on Arduino boards. The test results pointed out that the model is feasible for critical embedded environments since it provides the necessary functionality in this scenario without addition of an overhead in its communication

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

Um sistema de software que apresente problemas em sua execução pode gerar conseqüências desde um simples incômodo ao usuário, até desastres como a perda de uma sonda da NASA em Marte. As atividades de teste visam identificar erros nos sistemas de software, prevenindo estas conseqüências indesejáveis. Porém, os testes podem envolver entre 30% e 40% do esforço de desenvolvimento do sistema, e em sistemas críticos, seu custo pode ser de 3 a 5 vezes maior do que o custo combinado das demais atividades. Para tentar reduzir estes custos podemos automatizar parte das atividades. No presente caso, pretende-se minimizar os casos de teste gerados manualmente, utilizando uma técnica denominada verificação de modelos. Esta técnica consiste em verificar propriedades definidas formalmente através de expressões matemáticas, utilizando uma ferramenta de verificação que simula a execução do código. Além disso, um sistema que utilize um tratamento de condições excepcionais eficiente, tem sua manutenibilidade, robustez e confiabilidade melhoradas. Por isso, definimos propriedades relacionadas ao tratamento de exceções, como ponto de entrada para a verificação de modelos. Apresentamos um ambiente de testes criado para permitir a verificação destas propriedades com o verificador Java PathFinder e a exibição das estatísticas de cobertura de testes de acordo com o critério selecionado. Este ambiente facilita a execução dos testes, pois apresenta uma interface gráfica com o usuário que permite a configuração e execução dos testes sem que seja necessária a escrita de código pelo testador. Apresentamos também o resultado do uso deste ambiente para o teste de vários programas exemplo, utilizando desde código concorrente até diferentes estratégias de tratamento de exceção e discutimos as características, cuidados no uso e limitações das ferramentas utilizadas. / A software system that shows some failure at runtime execution may bring consequences that range from a simple user annoyance to great disasters such as the lost NASA probe on Mars. The test activities aim to find errors in software systems, preventing these undesirable consequences. However, tests may take between 30% and 40% of total development time, and on critical systems, its cost can be from 3 to 5 times greater than the combined cost of the other activities. In an effort to reduce these costs, we may automate some of the activities. In this work we intend to minimize test case manual generation, using a technique called model checking. This technique involves the checking of properties defined through the use of mathematical formulas, using a tool, that simulates code execution. In addition, a system with an efficient exception handling mechanism, has its maintainability, robustness and reliability enhanced. So, in this work we define exception handling related properties, as an input for model checking. We present a test tool created to allow checking of these properties using the Java PathFinder model checker, and to list the test coverage statistics, according to the selected test criteria. This tool makes easy the test execution, since it presents a graphical user interface that allows configuration and running of tests with no need to write any lines of code. We also show the results of running several tests with the GUI, using some programs implemented with concurrent code and several exception handling techniques and discuss the main features, pitfalls and limitations of the underlying tools.

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.

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.

Submitted by Erickson Alves (erickson.higor@gmail.com) on 2018-11-22T22:41:27Z No. of bitstreams: 1 capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) / Approved for entry into archive by PPGEE Engenharia Elétrica (mestrado_engeletrica@ufam.edu.br) on 2018-11-23T12:51:53Z (GMT) No. of bitstreams: 1 capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) / Rejected by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br), reason: O depósito está incompleto. É necessário fazer o upload da Dissertação, da Carta de Encaminhamento assinada pelo orientador. Segue orientações no link http://biblioteca.ufam.edu.br/servicos/teses-e-dissertacoes Dúvidas? ddbc@ufam.edu.br on 2018-11-23T14:01:34Z (GMT) / Submitted by Erickson Alves (erickson.higor@gmail.com) on 2018-11-29T00:18:47Z No. of bitstreams: 3 capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5) dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) / Approved for entry into archive by PPGEE Engenharia Elétrica (mestrado_engeletrica@ufam.edu.br) on 2018-11-29T13:12:34Z (GMT) No. of bitstreams: 3 capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5) dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-11-29T14:29:30Z (GMT) No. of bitstreams: 3 capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5) dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) / Made available in DSpace on 2018-11-29T14:29:30Z (GMT). No. of bitstreams: 3 capa de aprovação de Erickson.pdf: 159098 bytes, checksum: 53aadfbcf021e94fca0a6734d55714f0 (MD5) carta_encaminhamento.pdf: 373281 bytes, checksum: 057300b8bfec478dcee8902fab4d381b (MD5) dissertação.pdf: 627984 bytes, checksum: cfec6a01af6780eda1337a48143def43 (MD5) Previous issue date: 2018-09-14 / Este trabalho descreve uma nova abordagem para localizar falhas em programas concorrentes, a qual é baseada em técnicas de verificação de modelos limitada e sequencialização. A principal novidade dessa abordagem é a ideia de reproduzir um comportamento defeituoso em uma versão sequencial do programa concorrente. De forma a apontar linhas defeituosas, analizam-se os contraexemplos gerados por um verificador de modelos para o programa sequencial instrumentado e procura-se um valor para uma variável de diagnóstico, o qual corresponde a linhas reais no programa original. Essa abordagem é útil para aperfeiçoar o processo de depuração para programas concorrentes, já que ela diz qual linha deve ser corrigida e quais valores levam a uma execução bem-sucedida. Essa abordagem foi implementada como uma transformação código-a-código de um programa concorrente para um não-determinístico sequencial, o qual é então usado como entrada para ferramentas de verificação existentes. Resultados experimentais mostram que a abordagem descrita é eficaz e é capaz de localizar falhas na maioria dos casos de teste utilizados, extraídos da suíte da International Competition on Software Verification 2015. / Este trabalho descreve uma nova abordagem para localizar falhas em programas concorrentes, a qual é baseada em técnicas de verificação de modelos limitada e sequencialização. A principal novidade dessa abordagem é a ideia de reproduzir um comportamento defeituoso em uma versão sequencial do programa concorrente. De forma a apontar linhas defeituosas, analizam-se os contraexemplos gerados por um verificador de modelos para o programa sequencial instrumentado e procura-se um valor para uma variável de diagnóstico, o qual corresponde a linhas reais no programa original. Essa abordagem é útil para aperfeiçoar o processo de depuração para programas concorrentes, já que ela diz qual linha deve ser corrigida e quais valores levam a uma execução bem-sucedida. Essa abordagem foi implementada como uma transformação código-a-código de um programa concorrente para um não-determinístico sequencial, o qual é então usado como entrada para ferramentas de verificação existentes. Resultados experimentais mostram que a abordagem descrita é eficaz e é capaz de localizar falhas na maioria dos casos de teste utilizados, extraídos da suíte da International Competition on Software Verification 2015.

Com a presença cada vez maior de sistemas computacionais e novas tecnologias no cotidiano das pessoas, garantir que eles não falhem e funcionem corretamente tornou-se algo de extrema importância. Além de indicar a qualidade do sistema, assegurar seu bom funcionamento é essencial para se evitar perdas, desde financeiras até de vidas. Uma das técnicas utilizadas para esta finalidade é a chamada verificação formal de programas. A partir da especificação do sistema, descrita numa linguagem formal, são definidas propriedades a serem satisfeitas e que certificariam a qualidade do software. Estas propriedades devem então ser implementadas para uso num verificador, que é a ferramenta responsável por executar a verificação e informar quais propriedades foram satisfeitas e quais não foram; no caso das propriedades terem sido violadas, o verificador deve indicar aos desenvolvedores os possíveis locais com código incorreto no sistema. A desvantagem do uso da verificação formal é, além do seu alto custo, a necessidade de haver pessoas com experiência em métodos formais para definir propriedades a partir da especificação formal do sistema, e convertê-las numa representação que possa ser entendida pelo verificador. Este processo de definição de propriedades é particularmente complexo, demorado e suscetível a erros, por ser feito em sua maior parte de forma manual. Para auxiliar os desenvolvedores na utilização da verificação formal em programas escritos em Java, propomos neste trabalho a geração de representação de propriedades para uso direto num verificador. As propriedades a serem geradas são objetivos de teste derivados da especificação formal do sistema. Estes objetivos de teste descrevem o comportamento esperado do sistema que deve ser observado durante sua execução. Ao estabelecer que o universo de propriedades corresponde ao universo de objetivos de teste do programa, garantimos que as propriedades geradas em nosso trabalho descrevem o comportamento esperado do programa por meio de caminhos de execução que levam a um estado de aceitação da propriedade, ou a um estado de violação. Assim, quando o verificador checa o objetivo de teste, ele consegue dar como resultado o veredicto de sucesso ou falha para a propriedade verificada, além de dados da cobertura dos caminhos de execução do programa que podem ser usados para análise do comportamento do programa que levou ao sucesso ou falha da propriedade verificada. / The task of guaranteeing that computational systems do not fail and work correctly has become extremely important with the growing presence of new technologies in people\'s lives. Therefore, it is essential to ensure that such systems work properly to confirm their high-quality and to avoid financial and even life losses. One of the techniques used to this purpose is called formal verification of programs. From the system specification, which should be described in a formal language, we define properties that must be satisfied during system execution to guarantee the software quality. Then, these properties are checked using a verifier, which is the tool responsible for running the verification and for notifying whether the property was satisfied by the program; if the property was violated, it indicates to software developers the possible location of faults in the system. The disadvantages of using formal verification are the high cost to apply this technique in practice, and the necessity of having people with experience in formal methods to derive the properties from system specification and define them in a formal representation that can be read by a program verifier. This particular task of deriving a property from system specification and defining it to be checked by a verifier is complex, time-consuming and error-prone, since it is usually done by hand. To help software developers in the application of formal verification in Java programs, we propose in this work the generation of properties formal representation for direct use in a verifier. The generated properties are test purposes, which are derived from system formal specification and present the desirable system behavior that must be observed during the system execution. Establishing that the universe of properties correspond to the universe of test purposes of a program, we guarantee that the generated properties describe the expected program behavior through execution traces that lead to either an accept state or a refuse state. Thus, when the verifier checks the test purpose, it can give a success/fail verdict for the property, and provide traces coverage data that can be used to analyze the program behavior that led to that verdict.

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

Esta pesquisa é motivada pela crescente importância do reconhecimento automático de emoções, em especial através de sinais de voz, e suas aplicações em sistemas para interação homem-máquina. Neste contexto, são estudadas as emoções Felicidade, Medo, Nojo, Raiva, Tédio e Tristeza, além do estado Neutro, que são emoções geralmente consideradas como essenciais para um conjunto básico de emoções. São investigadas diversas questões relacionadas à análise de voz para reconhecimento de emoções, explorando vários parâmetros do sinal de voz, como por exemplo frequência fundamental (pitch), energia de curto prazo, formantes, coeficientes cepstrais e são testadas diferentes técnicas para a classificação, envolvendo reconhecimento de padrões e métodos estatísticos, como K-vizinhos mais próximos (KNN), Máquinas de Vetores de Suporte (SVM), Modelos de Misturas de Gaussianas (GMM) e Modelos Ocultos de Markov (HMM), destacando-se o uso de GMM como principal técnica utilizada por seu custo computacional e desempenho. Neste trabaho é desenvolvido um sistema de identificação em estágio único obtendo-se resultados superiores a diversos sistemas na literatura, com uma taxa de reconhecimento de até 74,86%. Além disso, recorre-se à psicologia e à teoria de emoções para incorporar-se a noção do espaço de emoções e suas dimensões a fim de desenvolver-se um sistema de classificação sequencial em três estágios, que passa por classificações nas dimensões Ativação, Avaliação e Domínio. Este sistema apresenta uma taxa de reconhecimento superior ao do sistema de único estágio, com até 82,41%, ao mesmo tempo em que é identificado um ponto de atenção no sistema de três estágios, que pode apresentar dificuldades na identificação de emoções que possuem baixo índice de reconhecimento em um dos estágios. Uma vez que existem poucos sistemas estado da arte que tratam o problema de verificação de emoções, um sistema também é desenvolvido para esta tarefa, obtendo-se um reconhecimento perfeito para as emoções Raiva, Neutro, Tédio e Tristeza. Por fim, é desenvolvido um sistema híbrido para tratar os problemas de verificação e de identificação em sequência, que tenta resolver o problema do classificador de três estágios e obtém uma taxa de reconhecimento de até 83%. / This work is motivated by the increase on the importance of automatic emotion recognition, especially through speech signals, and its applications in human-machine interaction systems. In this context, the emotions Happiness, Fear, Neutral, Disgust, Anger, Boredom and Sadness are selected for this study, which are usually considered essential for a basic set of emotions. Several topics related to emotion recognition through speech are investigated, including speech features, like pitch, energy, formants and MFCC as well as different classification algorithms that involve pattern recognition and stochastic modelling like K-Nearest Neighbours (KNN), Support Vector Machines (SVM), Gaussian Mixture Models (GMM) and Hidden Markov Models (HMM), where GMM is selected as the main technique for its computational cost and performance. In this work, a single-stage identification system is developed, which outperforms several systems in the literature, with a recognition rate of up to 74.86%. Besides, the idea of emotional space dimensions from Psychology and Emotion Theory is reviewed for the development of a sequential classification system with 3 stages, that passes through classifications on the Activation, Evaluation and Dominance dimensions. This system outperforms the single-stage classifier with a recognition rate of up to 82.41%, at the same time as a point of attention is identified, as this kind of system may show difficulties on the identification of emotions that show low recognition rates in a specific stage. Since there are few state of the art systems that handle emotion verification, a system for this task is also developed in this work, showing itself to be a perfect recognizer for the Anger, Neutral, Boredom and Sadness emotions. Finally, a hybrid system is proposed to handle both the verification and the identification tasks sequentially, which tries to solve the 3-stage classifier problem and shows a recognition rate of up to 83%.