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.

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 Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-23T13:23:08Z No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) / Made available in DSpace on 2018-08-23T13:23:08Z (GMT). No. of bitstreams: 1 DANIEL AGUIAR DA SILVA - DISS PPGCC 2006..pdf: 730843 bytes, checksum: e5d7ebe87ab82d200f68fb0b5b0df784 (MD5) Previous issue date: 2006-05-26 / Técnicas e ferramentas de testes formais baseados em modelos têm sido desenvolvidas para tornar mais rigoroso e eficiente o processo de teste de sistemas reativos com características de distribuição e concorrência. O não-determinismo inerente a estes sistemas torna os difíceis de serem testados, devido à alta complexidade de obtenção das configurações necessárias para execução dos casos de teste. As propriedades especificadas para estes sistemas são a base para a geração dos casos de teste de conformidade, que devem avaliar a correspondência entre modelo e código. Estas propriedades, denominadas objetivos de teste, devem ser especificadas de maneira a guiar a geração dos casos de teste. Entretanto, a especificação dos objetivos de teste a partir de modelos complexos como os destes sistemas ainda carece de técnicas e ferramentas apropriadas, tornando esta atividade propensa a erros. Os casos de teste podem assim, ter efetividade afetada em caso de erros na especificação dos objetivosdeteste. Comoobjetivodecontribuirparaasoluçãodesteproblema,estetrabalho apresenta técnica de geração de objetivos de teste para sistemas reativos, baseando-se na técnica de verificação de modelos CTL. A técnica proposta visa usufruir da eficiência dos algoritmos da verificação de modelos, por meio de sua adaptação para a análise destes, para a geração dos objetivos de teste. / Techniques and tools for model based testing have been developed to make the process of testing distributed concurrent reactive systems more efficient and rigorous. The inherent nondeterminism of these systems can make it difficult to test them due to the complex process of obtaining test cases configurations from models. To better guide the testing process, properties specified to these systems are used as basis for the test case generation. Such properties, called test purposes, shall be exhibitedby the implementation under test through test case execution. However, specifying test purposes from the common complex and large models of these systems suffers from the lack of appropriated tools and techniques, making it error-prone and inadequate. Thus, test cases based on such test purposes may be affected, getting no desirable soundness. Aiming at solving this problem, we present a technique for test purpose generation for reactive systems based on the CTL model checking technique. We aim at taking benefit from the efficiency of model checking algorithms to better analyze the models to generate the test purposes.