Verificação de modelos é uma das mais eficientes técnicas de verificação automática de sistemas. No entanto, apesar de poder lidar com verificações complexas, as ferramentas de verificação de modelos usualmente não fornecem informação alguma sobre como reparar inconsistências nestes modelos. Nesta dissertação, mostramos que abordagens desenvolvidas para a atualização de modelos CTL inconsistentes não são capazes de lidar com todos os tipos de alterações em modelos. Introduzimos então o conceito de revisão de modelos: uma abordagem baseada em revisão de crenças para o reparo de modelos inconsistentes em um contexto estático. Relacionamos nossa proposta com trabalhos clássicos em revisão de crenças. Definimos um operador de revisão de modelos e mostramos que este obedece postulados de racionalidade clássico de revisão de crenças. Propomos um algoritmo de revisão com base no algoritmo utilizado pela abordagem de atualização de modelos. Discutimos sobre problemas e limites do algoritmo proposto, e mostramos que essa estratégia de adaptação não é uma solução apropriada. / Model checking is one of the most robust techniques in automated system verification. But, although this technique can handle complex verifications, model checking tools usually do not give any information on how to repair inconsistent system models. In this dissertation, we show that approaches developed for CTL model update cannot deal with all kinds of model changes. We introduce the concept of CTL model revision: an approach based on belief revision to handle system inconsistency in a static context. We relate our proposal to classical works on belief revision. We define an operator for model revision and we show that it obeys the classical rationality postulates of belief revision. We propose an algorithm for model revision based on the algorithm used by the model update approach. We discuss problems and limitations of our proposed algorithm and show that this strategy of adaptation is not an appropriate solution.

O estudo de métodos estatísticos na avaliação de métodos diagnósticos tem aumentado consideravelmente nas últimas décadas. Desde o início, quando Yerushalmy (1947) publicou seu traba lho sobre confiabilidade do roentgeno grama na identificação da tuberculose, novas metodologias surgiram para que fosse possível a obtenção de valores de sensibilidade e especificidade de testes diagnósticos. A sensibilidade é definida como a probabilidade de o teste sob investigação fornecer um resultado positivo, dado que o indivíduo é realmen te portador da enfermidade. A especifi cidade, por sua vez, é definida como a probabilidade de o teste fornecer um resultado negativo, dado que o indivíduo está livre da enfermidade. Na prática, é comum ocorrerem situações em que uma proporção de indivíduos selecionados não pode ter o estado real da doença verificado, por se tratar de procedimentos invasivos, como no diagnóstico de câncer de pulmão, ou quaisquer outros casos em que são envolvidos riscos, portanto não praticá veis, nem éticos, ou ainda por serem de alto custo. Assim, em vez de se contornar o proble ma, muitos estudos de avaliação de performance de testes diagnósticos são elaborados apenas com informações de indivíduos verificados. Esse procedimento pode levar a resultados viesados. É o chamado viés de verificação, que consiste no cálculo de estimativas de sensibilidade e especi ficidade de testes diagnósticos quando apenas os indivíduos verificados pelo padrão ouro são inseridos na análise e os não verificados são descartados ou considerados livres de doença. Este trabalho apresenta uma revisão das metodologias já propostas para se calcularem a sensibilidade e a especificidade quando existe o viés de verificação, bem como uma análise detalhada da influência da proporção de indivíduos não verificados, o efeito do tamanho amostral e a escolha de distri buições a priori, quando utilizada a metodologia bayesiana, no cálculo dessas estimativas. Também foi introduzida uma metodologia, sob enfoque bayesiano, para a estimação das medidas de desempenho de dois testes diagnósticos, na presen ça do viés de verificação. / The study of statistical methods on diagnostic tests evaluation has increa sed in the last decades. Since the beginning, when Yerushalmy (1947) published his work about trustwor thiness of the roentgenogram in the identification of the tuberculosis, new methodologies had appeared and so that it was possible to get values of sensi tivity and specificity of diagnostic tests. Sensitivity is defined as the probability of the test under inquiry supply a positive result, since that the individual is really carrying on the disease. The specificity, in the other hand, is defined as the probability of the test supply a negative result, since that the individual is free of the disease. In practice, it is usual to occur situations where a proportion of selected individuals cannot have verified the real state of the illness, to the fact that the verification test can be an invasive procedure, as in the diagnosis of lung cancer, or any other cases where risks are involved, therefore not practicable, nor ethical, or still procedures with high cost. Thus, instead of solve the problem, many studies of evaluation of performance of diagnostic tests are elaborated only using the information of verified individuals. This procedure can leads to biased results. This is known as verification bias, that consists of the calculation of estimates of sensitivity and specificity of diagnostic tests when only the individuals verified by the gold standard test are inserted in the analysis and the unverified ones, discarded or considered that they are free of the disease. This work presents a revision of the methodologies already proposed to calculate sensitivity and the specificity in the presence of the verifi cation bias, as well as a detailed analysis of the influence of the propor tion of individuals not verified, the effect of the sample size and the influ ence of choosing different prior densi ties, when using the bayesian methodo logy, in the calculation of these estima tes. It was also introduced a bayesian methodology to estimate performance measures of two diagnostic tests when the verification bias is present.

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.

Submitted by Marlucy Farias Medeiros (marlucy.farias@unipampa.edu.br) on 2018-05-11T18:34:32Z No. of bitstreams: 1 Vinícius Bittencourt da Silva- 2018.pdf: 4217704 bytes, checksum: 062fdfd3aa89f2dbd2679f836c3bad2d (MD5) / Approved for entry into archive by Dayse Pestana (dayse.pestana@unipampa.edu.br) on 2018-05-14T11:58:52Z (GMT) No. of bitstreams: 1 Vinícius Bittencourt da Silva- 2018.pdf: 4217704 bytes, checksum: 062fdfd3aa89f2dbd2679f836c3bad2d (MD5) / Made available in DSpace on 2018-05-14T11:58:52Z (GMT). No. of bitstreams: 1 Vinícius Bittencourt da Silva- 2018.pdf: 4217704 bytes, checksum: 062fdfd3aa89f2dbd2679f836c3bad2d (MD5) Previous issue date: 2018-02-07 / Atualmente, o tempo de inserção de um produto de hardware no mercado é cada vez menor apesar do crescimento de sua complexidade. Portanto, é importante que o processo de construção seja cada vez mais rápido. Entre as medidas para ganhar desempenho a otimização do tempo despendido em verificação é fundamental, pois cerca de 70% do tempo de projeto é aplicado nessa atividade. Esse processo inicia-se juntamente com o desenvolvimento, pois, caso seja detectado um erro somente no estágio final de desenvolvimento é possível que haja atrasos para cumprir os prazos de entrega. Nesse sentido, este trabalho apresenta a USAG, uma ferramenta semi-automática desenvolvida para construir ambientes de verificação usando a metodologia UVM (a qual é a metodologia padrão atualmente) aplicada ao projeto de circuitos integrados escritos em SystemVerilog. Esta ferramenta vem para ajudar no processo de verificação de hardware acelerando a criação do ambiente de verificação, uma vez que ele gera as estruturas e interconexões da metodologia e produz os arquivos para simulação. Qualquer ferramenta que suporte SystemVerilog juntamente com a Metodologia UVM pode executar o ambiente de verificação gerado pela USAG. Além disso, a ferramenta é baseada na Web para ser acessível a partir de qualquer local sem a necessidade de um sistema operacional específico ou configuração para usá-la. Finalmente, são apresentados os resultados de ambientes de verificação UVM obtidos a partir da entrada de códigos fonte em SystemVerilog na USAG. A partir dos resultados obtidos e da análise da utilização por parte de testadores conclui-se que a USAG é eficaz no que tange os objetivos propostos. / Currently, the insertion time of a hardware pro ducts in the market is decreasing despite the growth of its complexity. Therefore, it is important that the construction process is getting faster and faster. Among the ways to gain performance, the optimization of the time spent in verification is fundamental, because ab out 70% of the project time is applied in this activity. This process starts with the development, because if an error is detected only in the final stage of development, there may be delays to comply with delivery times. In this way, this work presents USAG, a semi-automatic tool developed to construct verification environments using the UVM methodology (which is the current standard methodology) applied to the design of integrated circuits written in SystemVerilog. This tool comes to assist in the hardware verification process by accelerating the creation of the verification environment as it generates the structures and interconnections of the methodology and produces the files for simulation. Any tool that supports SystemVerilog together with the UVM Methodology can execute the verification environment generated by the USAG. In addition, the tool is web-based to be accessible from any lo cation without the need for a specific operating system or configuration to use it. Finally, the results of UVM verification environments obtained from the entry of source co des in SystemVerilog in USAG are presented.

A técnica de Desenvolvimento Orientado a Testes - DOT é uma técnica ágil para se desenvolver software, em que os testes de unidade vão sendo desenvolvidos antes das classes da aplicação. Essa técnica é executada em pequenos ciclos, entre os quais a refatoração do código, apoiada pelos testes de unidade, é uma técnica com um papel crucial para o aprimoramento da modelagem da aplicação. Nesse contexto em que os testes possuem papel fundamental, a refatoração do código de testes se mostra importante para que a modelagem do código de testes acompanhe a modelagem do código de produção. Porém, essa ainda é uma técnica pouco estudada. O uso da refatoração do código de teste é mostrado implicitamente na literatura, não havendo preocupação com a garantia de manutenção do comportamento do código de teste refatorado, nem sendo apresentado na literatura um conjunto substancial de refatorações específicas para código de testes. Neste trabalho busca-se realizar um estudo abrangente sobre a refatoração de código de teste, visando desenvolver esta técnica, possibilitando seu uso na prática para o aprimoramento contínuo do código de teste. Como resultado, espera-se ter um conjunto de ferramentas disponíveis para o desenvolvimento orientado a testes que inserem este tipo de refatoração explicitamente no ciclo de desenvolvimento. Dentre os principais benefícios esperados, pode-se citar: maior consciência da diferenciação entre refatoração de código de teste e de produção, maior segurança para a manutenção do comportamento original da classe de teste, e existência de catálogo de refatorações do código de teste, com a implementação da automatização de algumas delas.

A construção de software é um empreendimento de alto risco. Encontra na literatura que, no ano de 2009, 68% dos projetos de TI apresentaram falhas em prazo, custo ou qualidade. O Tribunal de Contas da União ressalta que a metodologia de desenvolvimento deve ser executada pelas organizações governamentais de forma sistemática e documentada, para permitir a avaliação e a melhoria do processo, com vistas à produção de software de qualidade. Neste contexto de metodologias para minimizar falhas, identificou-se em guias de boas práticas de gestão de projetos, livros e normas que tudo começa a partir da definição do escopo, sem o qual não é possível continuar o trabalho de gestão. Sendo assim, a deficiência da definição do escopo de um projeto aponta para um Modelo de Inspeção baseado em Checklist, com a finalidade de garantir que as principais informações geradas pelo grupo de processos de planejamento da gestão de escopo de projetos de sistema de TI, sejam observadas de forma adequada e estejam refletidas nos documentos produzidos por organizações públicas, mais especificamente do âmbito do Comando da Aeronáutica (COMAER). Para tanto, o trabalho é dividido em quatro partes: (1) identificar as informações relevantes para criar uma lista de verificação, a fim de auxiliar uma organização do Comando da Aeronáutica na execução do grupo de processos de planejamento da gestão de escopo, bem como, definir um método de inspeção baseado em uma técnica de leitura para ser utilizado na aplicação prática do modelo proposto; (2) apresentar a concepção do modelo da lista de verificação, a contextualização da mesma segundo o PMBOK e uma implementação do processo de inspeção para a aplicação prática do modelo proposto; (3) aplicar o modelo proposto através de dois exemplos de desenvolvimento de software, interno e terceirizado, por organizações militares da FAB; (4) avaliar o modelo proposto comparando os resultados obtidos com os problemas identificados pelos integrantes dos projetos nos exemplos estudados, realizando uma discussão acerca das conclusões obtidas. A tese conclui que o modelo desenvolvido: pode (1) minimizar os problemas identificados nos exemplos estudados; é (2) mais completo do que o PMBOK porque é necessário pesquisar informações em outras fontes de consulta para complementar as informações contidas neste guia de conhecimento; pode (3) prevenir os impactos de problemas legais desde as fases iniciais do projeto.

A crescente participação do software embarcado nas causas dos últimos acidentes espaciais evidencia a importância dos processos e técnicas de verificação e validação no desenvolvimento do software embarcado espacial. Neste contexto, este trabalho investiga a contribuição de duas técnicas de verificação para aplicações espaciais. A primeira técnica é o model checking baseado no uso da ferramenta UPPAAL. O UPPAAL adota a modelagem do sistema em autômatos temporizados e permite a verificação de propriedades especificadas em um subconjunto da linguagem CTL (Computational Tree Logic). A segunda técnica consiste especificação e aplicação de testes a partir de modelos de estados, considerando mais especificamente a metodologia CoFI (Conformance and Fault Injection). São utilizados como estudo de caso dois produtos de software espacial. Um dos produtos foi desenvolvido com o uso do model checking, enquanto o outro foi desenvolvido de acordo com as práticas atualmente aplicadas pelo grupo de computador de bordo do Departamento de Eletrônica Aeroespacial do INPE (Instituto Nacional de Pesquisas Espaciais). Ambos os produtos de software foram testados utilizando a metodologia CoFI. Cada produto consiste de uma implementação de dois serviços especificados na norma europeia PUS (Packet Utilization Standard). Estes serviços representam funcionalidades oferecidas por um computador de gerenciamento de bordo de satélites. As principais conclusões obtidas são que a metodologia CoFI contribui para o aprimoramento dos processos de verificação atualmente em uso no INPE, e que, o model checking associado à geração manual do código não implica na ausência de erros, porém ajuda a reduzir o número, mas não a criticidade de erros quando comparado com as práticas atualmente em uso.

Avionics system manufacturers are currently facing the problem of developing highly-integrated systems under economic pressures. In this scenario, the empirical approach, characterized by trial and error techniques, is not adequate since the correction of design flaws is often related to expensive re-work and schedule overruns. The evolution of airborne systems toward Integrated Modular Avionics (IMA) pushes the need for advanced methods that could enforce correctness of complex designs while minimizing the chances of introducing errors. Considering this problem, this work proposes a systematic conceptual design strategy based on formal methods, aiming at improving the development processes for IMA systems. The basic idea is to concentrate efforts on the construction, simulation, and formal analysis of a mathematical model for the new system at early development lifecycle phases. The proposed approach was exercised on a case study of practical avionics project in order to evaluate the drawbacks and advantages. Results suggest that this work could contribute to the aeronautics industry by offering alternative means to cope with complexity in modern avionics projects.

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.

Neste trabalho apresentamos uma implementação de revisão de crenças baseada em comparação de modelos (estados) em uma ferramenta de verificação automática de sistemas de estados finitos. Dada uma fórmula (na lógica CTL) inconsistente com o modelo do sistema, revisamos esse modelo de tal maneira que essa fórmula temporal se torne verdadeira. Como temos oito operadores temporais (AG, AF, AX, AU, EG, EF, EX e EU), foram criados algoritmos especícos para cada um deles. Como o modelo do sistema deriva do seu código na linguagem SMV, a sua revisão passa obrigatoriamente por mudanças na sua descrição. A nossa implementação contempla três tipos de mudanças: acréscimo de linhas, eliminação de linhas e mudança no estado inicial, sendo que as duas primeiras provocam modicações nas transições entre os estados que compõe o modelo. Alguns testes foram aplicados para comprovar a contribuição da revisão de crenças (revisão de modelos) como ferramenta de auxílio ao usuário durante o processo de modelagem de sistemas. / In this work we present an implementation of belief revision based on comparison of models (states) in a tool for automatic verication of nite state systems. Given a formula (in the language of CTL) inconsistent with the model of the system, we revise this model in such way that the temporal formula becomes valid. As we have eight temporal operators (AG, AF, AX, AU, EG, EF, EX and EU), specic algorithms for each one of them have been created. As the model of the system is related with its code in SMV language, its revision forces changes in its description. Our implementation contemplates three types of change: addition of lines, elimination of lines and change in the initial state, where the rst two cause modications in the transitions between the states of the model. Some tests were applied to prove the contribution of the belief revision (model revision) as aid-tool to the user during the process of systems modeling.