Exportar registro bibliográfico

Geração de propriedades sobre programas Java a partir de objetivos de teste (2015)

  • Authors:
  • Autor USP: HANAZUMI, SIMONE - IME
  • Unidade: IME
  • Sigla do Departamento: MAC
  • Subjects: ENGENHARIA DE PROGRAMAS; JAVA
  • Agências de fomento:
  • Language: Português
  • Abstract: 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.
  • Imprenta:
  • Data da defesa: 29.10.2015
  • Acesso à fonte
    How to cite
    A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas

    • ABNT

      HANAZUMI, Simone; MELO, Ana Cristina Vieira de. Geração de propriedades sobre programas Java a partir de objetivos de teste. 2015.Universidade de São Paulo, São Paulo, 2015. Disponível em: < http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748 >.
    • APA

      Hanazumi, S., & Melo, A. C. V. de. (2015). Geração de propriedades sobre programas Java a partir de objetivos de teste. Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748
    • NLM

      Hanazumi S, Melo ACV de. Geração de propriedades sobre programas Java a partir de objetivos de teste [Internet]. 2015 ;Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748
    • Vancouver

      Hanazumi S, Melo ACV de. Geração de propriedades sobre programas Java a partir de objetivos de teste [Internet]. 2015 ;Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748


Digital Library of Intellectual Production of Universidade de São Paulo     2012 - 2021