Informação relacionada a concertos de bugs tem sido explorada na construção de preditores de bugs cuja função é o suporte para a verificação de sistemas de software identificando quais elementos, como arquivos, são mais propensos a bugs. Uma grande variedade de métricas estáticas de código e métricas de mudança já foi utilizada para construir tais preditores. Dos muitos preditores de bugs propostos, a grande maioria foca em sistemas orientados à objeto. Apesar de orientação a objetos ser o paradigma de escolha para a maioria das aplicações, o paradigma procedural ainda é usado em várias — muitas vezes cruciais — aplicações, como sistemas operacionais e sistemas embarcados. Portanto, eles também merecem atenção. Essa dissertação extende o trabalho na área de predição de bugs ao avaliar e aprimorar preditores de bugs para sistemas procedurais de software. Nós proporcionamos três principais contribuições: (i) comparação das abordagens existentes de predição de bugs no contexto de sistemas procedurais, (ii) proposta de uso dos atributos de qualidade de software como atributos de predição no contexto estudado e (iii) avaliação dos atributos propostos em conjunto com a melhor abordagem encontrada em (i). Nosso trabalho provê, portanto, fundamentos para melhorar a performance de preditores de bugs no contexto de sistemas procedurais. / Information regarding bug fixes has been explored to build bug predictors, which provide support for the verification of software systems, by identifying fault-prone elements, such as files. A wide range of static and change metrics have been used as features to build such predictors. Many bug predictors have been proposed, and their main target is objectoriented systems. Although object-orientation is currently the choice for most of the software applications, the procedural paradigm is still being used in many—sometimes crucial—applications, such as operating systems and embedded systems. Consequently, they also deserve attention. This dissertation extends work on bug prediction by evaluating and tailoring bug predictors to procedural software systems. We provide three key contributions: (i) comparison of bug prediction approaches in context of procedural software systems, (ii) proposal of the use of software quality features as prediction features in the studied context, and (iii) evaluation of the proposed features in association with the best approach found in (i). Our work thus provides foundations for improving the bug prediction performance in the context of procedural software systems.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pòs-graduação em Engenharia de Automação e Sistemas, Florianópolis, 2011 / Made available in DSpace on 2012-10-26T05:05:01Z (GMT). No. of bitstreams: 1 296872.pdf: 1897409 bytes, checksum: 109437d10a6b10646d5638bb03afd255 (MD5) / projeto de sistemas embarcados criticos exige o uso de metodologias adequadas, visto que falhas no sistema podem causar danos catastroficos. Neste contexto se enquadra o projeto Topcased, o qual propõe uma série de ferramentas capazes de suportar a verificação formal de propriedades. A linguagem AADL tem um papel fundamental neste processo, pois sua utilização permite o emprego da transformação de modelos e a aplicação da verificação formal de propriedades. Entretanto, a especificação das propriedades de verificação e a análise dos seus resultados são ainda topicos em aberto. Esta dissertação visa suprir esta carência propondo um assistente para especificação de propriedades de verificação na linguagem AADL e uma interface para a visualização dos resultados de verificação, juntamente com um simulador de contraexemplos. O assistente construido classica as propriedades em padrões pre-definidos, utilizando uma linguagem natural ao usuário. Para validar as ferramentas desenvolvidas realizou-se um estudo de caso, o qual consistiu da especificação e verificação de propriedades de um sistema de marcapasso. Desta forma, este trabalho contribui com a melhoria da cadeia de verificação da linguagem AADL no escopo do projeto Topcased.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2013. / Made available in DSpace on 2014-08-06T17:34:32Z (GMT). No. of bitstreams: 1 323601.pdf: 3499862 bytes, checksum: 6f91e543fd542988c6ea40ea602ad442 (MD5) Previous issue date: 2013 / A flexibilidade de FPGAs baseadas em SRAM é uma opção atrativa para o projeto de sistemas embarcados. Contudo, estes sistemas críticos requerem a verificação funcional do projeto em HDL (Hardware Description Language) para assegurar o seu correto funcionamento. A verificação formal utilizando model checking representa um sistema em um modelo formal que pode ser automaticamente gerado por ferramentas de síntese. No entanto, as propriedades que descrevem o comportamento esperado, necessárias para provadores de modelo, são usualmente elaboradas de forma manual, o que é mais suscetível a erro humano, aumentando custo e tempo de verificação. Este trabalho apresenta uma nova abordagem para geração automática de propriedades para verificação de sistemas descritos em HDL. O estudo de caso industrial é o subsistema de comunicação de um satélite artificial que foi desenvolvido em parceria com o Instituto Nacional de Pesquisas Espaciais (INPE).<br> / Abstract: The flexibility of Commercial-Off-The-Shelf (COTS) SRAM-based FPGAs is an attractive option for the design of embedded systems. However, the functional verification of HDL-based designs is required and is of fundamental importance. Formal verification using model checking represents a system as formal model that are automatically generated by synthesis tools. On the other hand, the properties are represented by temporal logic expressions and are traditionally elaborated by hand, which is susceptible to human errors thus increasing the costs and verification time. This work presents a new method for automatic property generation for formal verification of Hardware Description Language (HDL) based systems. The industrial case study is a communication subsystem of an artificial satellite, which was developed in cooperation with the Brazilian Institute of Space Research (INPE).

Informação relacionada a concertos de bugs tem sido explorada na construção de preditores de bugs cuja função é o suporte para a verificação de sistemas de software identificando quais elementos, como arquivos, são mais propensos a bugs. Uma grande variedade de métricas estáticas de código e métricas de mudança já foi utilizada para construir tais preditores. Dos muitos preditores de bugs propostos, a grande maioria foca em sistemas orientados à objeto. Apesar de orientação a objetos ser o paradigma de escolha para a maioria das aplicações, o paradigma procedural ainda é usado em várias — muitas vezes cruciais — aplicações, como sistemas operacionais e sistemas embarcados. Portanto, eles também merecem atenção. Essa dissertação extende o trabalho na área de predição de bugs ao avaliar e aprimorar preditores de bugs para sistemas procedurais de software. Nós proporcionamos três principais contribuições: (i) comparação das abordagens existentes de predição de bugs no contexto de sistemas procedurais, (ii) proposta de uso dos atributos de qualidade de software como atributos de predição no contexto estudado e (iii) avaliação dos atributos propostos em conjunto com a melhor abordagem encontrada em (i). Nosso trabalho provê, portanto, fundamentos para melhorar a performance de preditores de bugs no contexto de sistemas procedurais. / Information regarding bug fixes has been explored to build bug predictors, which provide support for the verification of software systems, by identifying fault-prone elements, such as files. A wide range of static and change metrics have been used as features to build such predictors. Many bug predictors have been proposed, and their main target is objectoriented systems. Although object-orientation is currently the choice for most of the software applications, the procedural paradigm is still being used in many—sometimes crucial—applications, such as operating systems and embedded systems. Consequently, they also deserve attention. This dissertation extends work on bug prediction by evaluating and tailoring bug predictors to procedural software systems. We provide three key contributions: (i) comparison of bug prediction approaches in context of procedural software systems, (ii) proposal of the use of software quality features as prediction features in the studied context, and (iii) evaluation of the proposed features in association with the best approach found in (i). Our work thus provides foundations for improving the bug prediction performance in the context of procedural software systems.

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico, Programa de Pós-Graduação em Ciência da Computação, Florianópolis, 2012 / Made available in DSpace on 2013-06-25T21:01:52Z (GMT). No. of bitstreams: 1 312160.pdf: 2341823 bytes, checksum: 8d2b0ce79f3479d239bab9f53b2caa14 (MD5) / Nesta Dissertação de Mestrado, apresenta-se a proposta de um protocolo para autenticação de usuários, fazendo uso de biometria e smartcards. As principais características desse conjunto de protocolos são: prover um mecanismo próprio e integrado para cadastro e autenticação, assim como permitir a existência de diferentes papéis de usuários. Com a união destas duas características, almeja-se a obtenção de protocolos que possuam níveis aprimorados, não apenas de segurança, mas também de gerenciamento. Seu desenvolvimento é norteado pela adoção de uma metodologia própria ao projeto de protocolos de segurança. As seguintes etapas fazem parte desta metodologia: projeto inicial, prototipação, implantação, modelagem formal e verificação. A modelagem formal é feita em Lógica de Primeira Ordem. Os modelos lógicos criados são, posteriormente, alvo de verificação com auxílio de um provador automático de teoremas (em nosso caso, o SPASS). De modo a antecipar as ações de um atacante em potencial, seus possíveis movimentos são também alvo de formalização, resultando na criação de um modelo lógico próprio. Logo após, tem início a etapa de verificação, a qual consiste no teste de conjecturas sobre os modelos lógicos. O resultado deste teste permite a extração de fatos (certezas) sobre nosso conjunto de protocolos. Em última análise, estes fatos são a comprovação da resistência do protocolo a padrões conhecidos de ataque. Com a finalidade de propiciar uma visão geral da temática da verificação de protocolos de segurança, este trabalho também apresenta uma revisão dos métodos disponíveis, não se limitando apenas àqueles efetivamente utilizados neste estudo. Ademais, todo o material relativo às modelagens formais e respectivas provas é incluído como anexos.<br> / Abstract : In this Master Thesis, a proposal for a set of authentication protocols through the use of biometrics and smartcards is presented. The main characteristics of such protocols are: to provide their own integrated mechanism for user registration and authentication, as well as to differentiate the existent user roles. By combining these characteristics, we aim at creating protocols with, not only improved security levels, but also with flexible management. Their development is guided by the adoption of a proper methodology for the security protocols' project. The following steps make part of it: initial design, prototyping, deployment, formal modelling and verification. The formal modelling is carried out in First-Order Logic. The logic models created are subsequently targeted of verification with the assistance of an automated theorem prover (in this case, SPASS). To anticipate the actions from a potential attacker, his characteristics are also target of formalisation, resulting in his own logic model. After, we proceed with the verification which consists on testing conjectures upon the logic models. The results collected with those tests allow the extraction of facts about our set of protocols. In a last instance, such facts are the evidence of the protocol's resistance to well-known attack patterns. In order to provide a broader view of the subject of security protocol verification, this work also reviews all the available methods. Not limiting to those already used in this study. In addition, every piece of material related to the formal modelling and respective proofs is included as appendices.

Informação relacionada a concertos de bugs tem sido explorada na construção de preditores de bugs cuja função é o suporte para a verificação de sistemas de software identificando quais elementos, como arquivos, são mais propensos a bugs. Uma grande variedade de métricas estáticas de código e métricas de mudança já foi utilizada para construir tais preditores. Dos muitos preditores de bugs propostos, a grande maioria foca em sistemas orientados à objeto. Apesar de orientação a objetos ser o paradigma de escolha para a maioria das aplicações, o paradigma procedural ainda é usado em várias — muitas vezes cruciais — aplicações, como sistemas operacionais e sistemas embarcados. Portanto, eles também merecem atenção. Essa dissertação extende o trabalho na área de predição de bugs ao avaliar e aprimorar preditores de bugs para sistemas procedurais de software. Nós proporcionamos três principais contribuições: (i) comparação das abordagens existentes de predição de bugs no contexto de sistemas procedurais, (ii) proposta de uso dos atributos de qualidade de software como atributos de predição no contexto estudado e (iii) avaliação dos atributos propostos em conjunto com a melhor abordagem encontrada em (i). Nosso trabalho provê, portanto, fundamentos para melhorar a performance de preditores de bugs no contexto de sistemas procedurais. / Information regarding bug fixes has been explored to build bug predictors, which provide support for the verification of software systems, by identifying fault-prone elements, such as files. A wide range of static and change metrics have been used as features to build such predictors. Many bug predictors have been proposed, and their main target is objectoriented systems. Although object-orientation is currently the choice for most of the software applications, the procedural paradigm is still being used in many—sometimes crucial—applications, such as operating systems and embedded systems. Consequently, they also deserve attention. This dissertation extends work on bug prediction by evaluating and tailoring bug predictors to procedural software systems. We provide three key contributions: (i) comparison of bug prediction approaches in context of procedural software systems, (ii) proposal of the use of software quality features as prediction features in the studied context, and (iii) evaluation of the proposed features in association with the best approach found in (i). Our work thus provides foundations for improving the bug prediction performance in the context of procedural software systems.

[pt] Em um sistema de informação, falhas podem ocorrer pela diferença de entendimento das partes envolvidas em relação ao significado de um dado. Este é um problema bem conhecido pela engenharia de software, e defeitos deste tipo já foram responsáveis por falhas catastróficas, como a do Mars Climate Orbiter em 1999. O atual cenário de intercâmbio e processamento de dados, com grande volume de informação e heterogeneidade de participantes, cria um estado de suscetibilidade a estes defeitos. Entretanto, as técnicas de garantia de qualidade de software são tipicamente dirigidas à estrutura e às propriedades físicas dos dados, e não são eficientes ao observar questões semânticas. Este trabalho tem como intuito avaliar o uso de análise estática na detecção de conflitos semânticos em tipos de dados, e para validar sua eficácia esta abordagem foi comparada com outras técnicas de garantia de qualidade em um estudo qualitativo. A ferramenta de análise estática VERITAS (VERIficador estTÁtico Semântico) e a notação SemTypes foram desenvolvidas exclusivamente para tratar do problema de conflitos semânticos, adicionando controle de tipo semântico aos tipos reconhecidos por compiladores, e são apresentadas neste trabalho. / [en] Within information system, faults can occur by the difference in understanding of the parties involved regarding the meaning of data. This is a well-known problem for software engineering and defects of this type have been responsible for catastrophic failures, such as the Mars Climate Orbiter in 1999. The current scenario of data processing and exchange, with high information traffic volume and heterogeneous participants, increases system’s vulnerability to these defects. Besides that, techniques of software quality assurance are typically oriented to data structure and physical properties, failing to efficiently address semantics issues. This work has the objective to evaluate the use of static analysis to detect semantic conflicts in data types, investigating its efficacy through an qualitative study comparing different software quality assurance approaches. The static analysis tool VERITAS (VERIficador esTÁtico Semântico) and the SemTypes notation were exclusively developed to address the problem of semantic conflicts - adding a semantic control to the types recognized by compilers – and are presented in this work.

[pt] Neste trabalho propomos uma arquitetura para a verificação formal de protocolos e algoritmos distribuídos. Esta pode ser vista como uma camada mais abstrata sobre o processo tradicional de verificação formal, onde temos a especificação e propriedade a serem verificadas, o verificador e o resultado retornado por este. O objetivo é simplificar o processo de especificação e verificação formal de protocolos e algoritmos distribuídos através de um ambiente mais dedicado. A parte principal desta arquitetura é a linguagem de especificação LEP, que contém construções de domínio-especifíco para simplificar a especificação destes sistemas. Outra característica desta linguagem é separar as especificações da topologia e do protocolo propriamente dito. Acreditamos que esta separação é válida pois torna mais clara a intenção das partes e ainda permite, por exemplo, o reuso de uma topologia entre diferentes especificações de protocolos. Assim, visamos oferecer uma linguagem cujos exemplos de especificações devem se assemelhar às descrições de algoritmos encontradas nos livros didáticos. Além disso, de forma a se ter a entrada e a saída dos verificadores formais de forma a obter a saída no nível de abstração de LEP. / [en] In this work we propose an architecture for the formal verification of protocols and distribued algoritms. This can be see as a more abstract layer over the ordinary process of formal verification, where we have just the specification of the protocol and properties to be verified, and the formal tool. Our goal is to simplifu the specification and formal verification of protocols and distributed algorithms through a dedicated environment. The core of the architecture is its input specification language (Lep), which provides domain-specific constructions for simplifying the specification of those systems. With LEP the specification of the protocol and the specification of the topology to be referred to protocol are given separetely. We feel that this division improves the legibility of both and allows the reuse of the specification of a topology among distinct protocols. Using this approach we try to offer a language whose specifications should be similar to the descriptions of the algorithms found on the didactic books. Moreover, in order to have the input and output of the architecture compatible, we also propose a way of processing the result of the formal verification tool. Then we could have the result on the abstract level of LEP.

[pt] O crescimento e a popularidade da web impulsionaram o desenvolvimento de softwares baseados em rede. O uso de sistemas multiagentes (SMAs) nesse contexto é considerado uma abordagem promissora em vem sendo aplicada em diferentes áreas tais como: segurança, missões ou cenários críticos de negócios, monitoramento avançado de ambientes e pessoas, etc., o que significa que analisar as escolhas que este tipo de software pode fazer torna-se crucial. Contudo, as metodologias propostas até o momento pela Engenharia de Software Orientada a Agentes (AOSE) concentraram seus esforços principalmente no desenvolvimento de abordagens disciplinadas para analisar, projetar e implementar um SMA e pouca atenção tem sido dada a forma como tais sistemas podem ser testados. Além disso, no que se refere a testes envolvendo agentes de software, algumas questões relacionadas à observabilidade e a controlabilidade dificultam a tarefa de verificação do comportamento, tais como: (i) a autonomia do agente em seu processo deliberativo; (ii) o fato das crenças e objetivos do agente estarem embutidos no próprio agente, dificultam a observação e controle do comportamento e; (iii) problemas associados à cobertura dos testes. Neste trabalho é apresentada uma nova abordagem para testes unitários de agentes BDI escritos em BDI4JADE baseadas na combinação e adaptação das ideias suportadas pelo JAT Framework, um framework de testes para agentes escritos em JADE e no modelo de faltas proposto por Zhang. / [en] The growth and popularity of the Web has fueled the development of software-based network. The use of multi-agent systems (MAS) in this context is considered a promising approach has been applied in different areas such as security, or mission critical business scenarios, enhanced monitoring of environments and people, etc., which means analyzing the choices that this type of software can become crucial. However, the methodologies proposed so far by the Software Engineering Oriented Agents (AOSE) focused their efforts mainly on developing disciplined approach to analyze, design and implement an SMA and little attention has been given to how such systems can be tested. Furthermore, with regard to tests involving software agents, some issues related to the controllability and observability difficult the task of checking the behavior, such as: (i) the duration of the agent in its decision-making process; (ii) the fact of the agent s beliefs and goals are embedded in the agent itself, hampering the observation and control of behavior; (iii) problems associated with test coverage. In this research a novel approach for unit testing of agents written in BDI4JADE BDI based on the combination and arrangement of ideas supported by JAT Framework, a framework for testing agents written in JADE and fault model proposed by Zhang is displayed.

[pt] Os defeitos nas especificações de requisitos podem ter consequências graves durante o ciclo de vida de desenvolvimento de software. Alguns deles resultam em uma falha geral do projeto devido a características de qualidade incorretas ou ausentes, como segurança. Existem várias preocupações que tornam a segurança difícil de lidar; por exemplo, (1) quando as partes interessadas discutem os requisitos gerais nas reuniões, muitas vezes não estão cientes que também devem discutir tópicos relacionados à segurança. (2) Normalmente as equipes de desenvolvimento não possuem conhecimentos de segurança suficientes. Isto geralmente leva a aspectos de segurança não especificados ou mal definidos. Essas preocupações tornam-se ainda mais desafiadoras em contextos de desenvolvimento ágil, nos quais a documentação leve geralmente está envolvida. O objetivo desta dissertação é projetar e avaliar uma abordagem para suportar a revisão de aspectos relacionados à segurança em especificações de requisitos ágeis de aplicativos web. A abordagem projetada considera estórias de usuário e especificações de segurança como entradas e relaciona essas estórias de usuário a propriedades de segurança através de técnicas de Processamento de Linguagem Natural. Com base nas propriedades de segurança relacionadas, nossa abordagem identifica os requisitos de segurança de alto nível do OWASP (Open Web Application Security Project) a serem verificados e gera uma técnica de leitura focada para dar suporte aos revisores na detecção de defeitos. Avaliamos nossa abordagem rodando dois experimentos controlados. Comparamos a eficácia e a eficiência de inspetores novatos que verificam aspectos de segurança em requisitos ágeis usando nossa técnica de leitura contra o uso da lista completa de requisitos de segurança de alto nível do OWASP. Os resultados (estatisticamente significativos) indicam que o uso da nossa abordagem tem um impacto positivo (com tamanho de efeito muito grande) no desempenho dos inspetores em termos de eficácia e eficiência. / [en] Defects in requirements specifications can have severe consequences during the software development life cycle. Some of them result in overall project failure due to incorrect or missing quality characteristics such as security. There are several concerns that make security difficult to deal with; for instance, (1) when stakeholders discuss general requirements in (review) meetings, they are often not aware that they should also discuss security-related topics, and (2) they typically do not have enough expertise in security. This often leads to unspecified or ill-defined security aspects. These concerns become even more challenging in agile development contexts, where lightweight documentation is typically involved. The goal of this dissertation is to design and evaluate an approach to support reviewing security-related aspects in agile requirements specifications of web applications. The designed approach considers user stories and security specifications as input and relates those user stories to security properties via Natural Language Processing (NLP). Based on the related security properties, our approach then identifies high-level security requirements from the Open Web Application Security Project (OWASP) to be verified and generates a focused reading technique to support reviewers in detecting defects. We evaluate our approach via two controlled experiment trials. We compare the effectiveness and efficiency of novice inspectors verifying security aspects in agile requirements using our reading technique against using the complete list of OWASP high-level security requirements. The (statistically significant) results indicate that using our approach has a positive impact (with very large effect size) on the performance of inspectors in terms of effectiveness and efficiency.