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
-
ABNT
HANAZUMI, Simone. Geração de propriedades sobre programas Java a partir de objetivos de teste. 2015. Tese (Doutorado) – Universidade de São Paulo, São Paulo, 2015. Disponível em: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748. Acesso em: 25 abr. 2024. -
APA
Hanazumi, S. (2015). Geração de propriedades sobre programas Java a partir de objetivos de teste (Tese (Doutorado). 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. Geração de propriedades sobre programas Java a partir de objetivos de teste [Internet]. 2015 ;[citado 2024 abr. 25 ] Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748 -
Vancouver
Hanazumi S. Geração de propriedades sobre programas Java a partir de objetivos de teste [Internet]. 2015 ;[citado 2024 abr. 25 ] Available from: http://www.teses.usp.br/teses/disponiveis/45/45134/tde-23122015-094748 - Ambiente integrado para verificação e teste da coordenação de componentes tolerantes a falhas
- Coordinating exceptions of Java systems: implementation and formal verification
- Generation of Java programs properties from test purposes
- Using formal verification to reduce test space of fault-tolerant programs
- OConGraX: automatically generating data-flow test cases for fault-tolerant systems
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
