O teste de software é uma atividade essencial para verificação da qualidade do produto. A grande dificuldade, porém, é a impossibilidade de se testar todos os estados que o software pode assumir, tornando-se necessário desenvolver heurísticas para atividade de teste, de forma que seja testado um subconjunto dos estados tomado como representativo. Para isto, deve-se saber avaliar o quão aceitável está o conjunto de testes. Os critérios de adequação de teste estabelecem um conjunto mínimo de regras que devem ser satisfeitas pelo conjunto de teste, de forma a analisar sua adequação, ou sua necessidade de refinamento. Dentre os critérios de adequação de teste, serão abordados neste trabalho o MC/DC (Modified Condition / Decision Coverage) e o Teste de Mutação, fazendo-se uma comparação entre ambos através da propriedade de inclusão. Pretende-se demonstrar que o Teste de Mutação, com o projeto de alguns operadores de mutação específicos, é capaz de incluir o MC/DC. A discussão é trazida para o nível dos requisitos sob a forma de modelos, que antecipa a utilização dos critérios para uma etapa anterior à geração de código no desenvolvimento de software. Será desenvolvido um algoritmo gerador de mutantes em modelos gerados na ferramenta SCADE de tal forma que ao matarem-se todos os modelos mutantes, automaticamente o MC/DC no modelo original será satisfeito.

Este trabalho apresenta um ambiente de laboratório de acesso remoto, denominado WebLab, cujo objetivo principal é possibilitar a realização e controle em tempo real de experimentos, usando como meio a internet. Esse ambiente, que foi testado e validado em aplicações ligadas ao ensino de física, pode ser utilizado com as devidas adaptações, em qualquer área do conhecimento. Do ponto de vista da Engenharia da Computação, a verificação formal da arquitetura do WebLab foi realizada usando uma abordagem de redes de Petri Colorida. As especificações e verificações formais do ambiente baseadas nessas redes, permitiram constatar que as funcionalidades planejadas do modelo pedagógico são realizadas, antes mesmo de sua implementação.

Este trabalho tem como objetivo a análise da aplicação de métodos formais para a modelagem e verificação de produtos de software embarcado para aplicações aeroespaciais de tempo-real. Como abordagem para modelagem, utilizam-se autômatos temporizados e a ferramenta UPPAAL. A verificação do modelo construído é realizada por meio da abordagem de model-checking, utilizando um conjunto de propriedades definidas em CTL que refletem os requisitos do sistema em análise. Particular ênfase é dada ao problema de verificação de requisitos de tempo no sistema em análise. Para tanto, a metodologia proposta inclui a modelagem não apenas do aplicativo de software mas também do sistema operacional que gerencia os diversos processos executados pelo software. Como estudo de caso utiliza-se o computador de bordo de um simulador de satélite com um grau de liberdade. Este estudo de caso inclui a determinação dos tempos utilizados para execução do software aplicativo e dos tempos utilizados pelo sistema operacional. Além da verificação dos requisitos de tempo do sistema, o estudo de caso apresenta uma análise de sensibilidade destes requisitos frente à variação de alguns parâmetros do sistema. Baseado nos resultados do estudo de caso, apontam-se as vantagens e limitações do uso da abordagem de model checking para verificação de sistemas de tempo real para aplicações aeroespaciais.

Este trabalho propõe e avalia a aplicação da técnica de verificação model checking no desenvolvimento de software embarcado de satélites universitários. Inicialmente, apresenta uma revisão do cenário atual de projetos de satélites universitários, com foco no computador de bordo e a adoção de normas para este subsistema. Esta revisão aponta que os satélites universitários tendem a adotar estratégias simples e de baixo custo para garantir dependabilidade, o que torna o uso de model checking uma solução atrativa, viável e factível para verificação da especificação de software embarcado crítico destes satélites. Como estudo de caso, utiliza-se a ferramenta UPPAAL, baseada em autômatos temporizados, para verificação da especificação de software do módulo de comunicação (CM) do computador de bordo do satélite universitário ITASAT. Este módulo executa programas sequenciais que contemplam: recepção de telecomando, execução de comandos diretos, verificação dos principais canais e envio de telemetria. A primeira etapa do processo de aplicação de model checking consistiu na modelagem, de forma isolada, de cada um dos dois submódulos do CM. Para cada modelo, foram feitas verificações de propriedades básicas e dos requisitos de software. Foras discutidas estratégias práticas para contornar o problema de explosão de número de estados. Numa segunda etapa, os modelos dos dois submódulos foram integrados em um único modelo. Para o modelo integrado, foram verificadas as propriedades de alcançabilidade, ausência de deadlock e propriedades referentes a interação entre os módulos. Apesar das restrições de comandos disponíveis, devido ao problema de explosão de estados, foram criados cenários de verificação para observar a relação entre módulos. Ao final, conclui-se que a utilização do model checking permitiu a identificação de erros e de oportunidades de melhoria na especificação de requisitos e que é uma solução viável para atender a proposta de satélites universitários.

O domínio de sistema de software crítico embarcado requer atividades de Engenharia Reversa de Software especializadas para atender características típicas a esse tipo de sistema. A Engenharia Reversa de Software para sistemas de software críticos embarcados não tem focado na análise temporal de tais sistemas. Um dos desafios é a construção de um modelo para análise com detalhes suficientes para expressar as propriedades temporais que são de interesse de uma atividade de Engenharia Reversa de Software. Este trabalho propõe uma abordagem de Engenharia Reversa de Software para sistema de software crítico embarcado visando propiciar um entendimento dos aspectos temporais e segurança do software por meio de um modelo formal, a fim de prover o entendimento completo de tais aspectos. A solução é essencialmente baseada nas atividades de verificação formal de software e modelo e em uma base de conhecimento para armazenar os resultados dessas atividades. Os resultados da aplicação da abordagem em um software aeroespacial sugerem que a abordagem é viável de ser executada e correta ao atingir seu objetivo principal, que é aumentar a compreensão geral do sistema tanto para manutenção, evolução bem como para desenvolvimento de software novo.

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.

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.

MARINHO, Fabiana Gomes. PRECISE - Um processo de verificação formal para modelos de características de aplicações móveis e sensíveis ao contexto. 2012. 181 f. Tese (Doutorado em ciência da computação)- Universidade Federal do Ceará, Fortaleza-CE, 2012. / Submitted by Elineudson Ribeiro (elineudsonr@gmail.com) on 2016-07-12T19:42:02Z No. of bitstreams: 1 2012_tese_fgmarinho.pdf: 5103390 bytes, checksum: dd5da728cc7af5f3e122c8c7afaf49aa (MD5) / Approved for entry into archive by Rocilda Sales (rocilda@ufc.br) on 2016-07-25T11:39:31Z (GMT) No. of bitstreams: 1 2012_tese_fgmarinho.pdf: 5103390 bytes, checksum: dd5da728cc7af5f3e122c8c7afaf49aa (MD5) / Made available in DSpace on 2016-07-25T11:39:31Z (GMT). No. of bitstreams: 1 2012_tese_fgmarinho.pdf: 5103390 bytes, checksum: dd5da728cc7af5f3e122c8c7afaf49aa (MD5) Previous issue date: 2012 / SPLc have been used to develop different types of applications, including the ones that run on mobile devices and are able to adapt when the context elements in which they are located change. These applications can change due to variations in their execution environment and inconsistent adaptations can occur, compromising the expected behavior. Then there is a need for creating a verification process to check the correctness and consistency of these SPLs as well as to check the correctness of both derived products and adapted products from these SPLs. Thus, this work proposes PRECISE - A Formal Verification Process for Feature Models of Mobile and Context-Aware Applications. PRECISE helps to identify defects in the variability modeling of an SPL for mobile and context-aware applications, minimizing problems that can take place during the execution of products generated from this SPL. It is worth noting that PRECISE is defined based on a formal specification and a set of well-formedness properties developed using First-Order Logic, which are prerequisites for the achievement of an unambiguous variability modeling. To evaluate PRECISE, a validation is performed from the formal specification and well-formedness properties defined in the process. This validation intends to show that PRECISE is able to identify defects, anomalies and inconsistencies in a variability model of an SPL for mobile and context-aware applications. In this validation, five different techniques are used: UML Profile, OCL, Propositional Logic, Prolog and Simulation. While minimizing the defects and inconsistencies in the variability models of an SPL, PRECISE still benefits from the generality and flexibility intrinsic to the formal notation used in its specification. / As LPSs, além do seu uso em aplicações tradicionais, têm sido utilizadas no desenvolvimento de aplicações que executam em dispositivos móveis e são capazes de se adaptarem sempre que mudarem os elementos do contexto em que estão inseridas. Essas aplicações, ao sofrerem alterações devido a mudanças no seu ambiente de execução, podem sofrer adaptações inconsistentes e, consequentemente, comprometer o comportamento esperado. Por esse motivo, é essencial a criação de um processo de verificação que consiga checar a corretude e a consistência dessas LPSS, bem como checar a corretude tanto dos produtos derivados como dos produtos adaptados dessas LPSs. Sendo assim, nesta tese de doutorado é proposto o PRECISE - um Processo de Verificação Formal para Modelos de Características de Aplicações Móveis e Sensíveis ao Contexto. O PRECISE auxilia na identificação de defeitos na modelagem da variabilidade de uma LPS para aplicações móveis e sensíveis ao contexto e, assim, minimiza problemas que ocorreriam durante a execução dos produtos gerados a partir dessa LPS. É importante ressaltar que o PRECISE é definido com base em uma especificação formal e em um conjunto de propriedades de boa formação elaborados usando Lógica de Primeira Ordem. Essa especificação é um pré-requisito para a realização de uma modelagem da variabilidade sem ambiguidades. Para avaliar o PRECISE, uma validação é realizada a partir da especificação formal e das propriedades de boa formação definidas no processo. Essa validação tem como objetivo mostrar que o PRECISE consegue identificar defeitos, anomalias e inconsistências existentes em um modelo de variabilidades de uma LPS para aplicações móveis e sensíveis ao contexto. Nessa validação, cinco técnicas diferentes são utilizadas: Perfil UML, OCL, Lógica Proposicional, Prolog e Simulação. Além de minimizar os defeitos e inconsistências dos modelos de variabilidades das LPSs, o PRECISE ainda se beneficia da generalidade e flexibilidade intrínsecas à notação formal usada na sua especificação.

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.

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:38Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2018-03-21T17:40:50Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) / Made available in DSpace on 2018-03-21T17:40:50Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação_Raimundo W. R. Melo.pdf: 1511352 bytes, checksum: 35f1429da9fc237f23a6e983f4c6abd9 (MD5) Previous issue date: 2017-08-10 / FAPEAM - Fundação de Amparo à Pesquisa do Estado do Amazonas / The use of embedded systems, i.e., computer systems focused on performing specific functions in larger (electronic or mechanical) systems, has been growing lately, and ensuring the robustness of such systems has become increasingly important. There are several techniques to ensure that a system is released without errors. In particular, formal verification of programs is proving itself to be effective in the search for failures. In this work, an induction-proof algorithm is described, which combines k-induction and invariants to verify and refute safety properties in embedded ANSI-C software. Moreover, the proposed k-induction-based approach infers invariants in the program to assist in verification tasks, using constraint refinement (i.e., polyhedral) to specify pre- and post-conditions. We adopted two invariant generators to produce such and feed the k-induction algorithm, which is implemented in the Efficient SMT-Based Context-Bounded Model Checker tool. Public benchmarks were used to assess the effectiveness of our approach. In addition, a comparison to other state-of-the-art verification tools using a set of benchmarks from the International Competition for Software Verification in addition to embedded systems applications. Experimental results have shown that the proposed approach, with and without invariants, can verify a wide variety of safety properties in programs with loops and embedded software from telecommunications, control systems, and medical domains. / O uso de sistemas embarcados, sistemas computacionais especializados para execução em sistemas eletrônicos ou mecânicos tem crescido de forma vertiginosa devido a utilização cada vez mais intensa de sensores, interfaces de rede e protocolos de comunicação em diversas áreas. Por isso, é cada vez mais importante garantir a robustez desses sistemas, uma vez que estão se tornando mais complexos e integrados. Existem várias técnicas para garantir que um sistema seja entregue ao cliente sem erros, em particular, a verificação formal dos programas tem se revelado eficaz na busca de falhas. Neste trabalho é descrito um algoritmo de indução matemática conhecido como k-induction combinado ao uso de invariantes para verificar e refutar propriedades de segurança em programas desenvolvidos na linguagem ANSI-C. Em particular, a abordagem proposta infere invariantes no programa para auxiliar na verificação de programas ANSI-C através da técnica de indução matemática através do refinamento de restrição (i.e, poliédrico) para especificar pré- e pós-condições. No método proposto, adotamos dois geradores de invariantes para produzir e alimentar o algoritmo de indução matemática o qual é implementado na ferramenta Efficient SMT-Based Context-Bounded Model Checker. A motivação para a combinação de invariantes com o algoritmo de indução matemática é fechar um gap na verificação formal de programas que possuam variáveis globais, além de programas com loops que possuem desvios condicionais e o número de iterações é desconhecido. PIPS e PAGAI são as ferramentas utilizadas para analisar o código e produzir invariantes indutivas responsáveis por guiar o algoritmo de indução matemática na verificação do benchmark, sendo este o principal desafio do método proposto. Para avaliar a eficácia da abordagem proposta neste trabalho, além de aplicações de Sistemas Embarcados foram utilizados benchmarks públicos disponibilizados pela Competição Internacional de Verificação de Software onde participam Universidades, pesquisadores, estudandantes de doutorado de várias partes do mundo, e fornece amplo conjunto de casos de teste para verificação. Além disso, foram utilizadas ferramentas estado-da-arte para a comparação dos resultados e, assim mensurar a eficácia do método proposto. Os resultados experimentais foram positivos e mostraram que o algoritmo de indução matemática com invariantes pode verificar uma grande variedade de propriedades de segurança em programas com loops e aplicações de sistemas embarcados de telecomunicações, sistemas de controle e dispositivos médicos.