Submitted by Johnny Rodrigues (johnnyrodrigues@ufcg.edu.br) on 2018-08-31T22:55:43Z No. of bitstreams: 1 CATUXE VARJÃO DE SANTANA OLIVEIRA - PPGCC DISSERTAÇÃO 2013..pdf: 11354934 bytes, checksum: 6a23f31ef43ba211aeaa89eb36061a43 (MD5) / Made available in DSpace on 2018-08-31T22:55:43Z (GMT). No. of bitstreams: 1 CATUXE VARJÃO DE SANTANA OLIVEIRA - PPGCC DISSERTAÇÃO 2013..pdf: 11354934 bytes, checksum: 6a23f31ef43ba211aeaa89eb36061a43 (MD5) Previous issue date: 2013-03-15 / A escrita de especificações formais por contratos é uma maneira confiável e prática de construir softwares, em que desenvolvedores e clientes mantêm um acordo contendo direitos e obrigações a serem cumpridos. Essas responsabilidades são expressas basicamente através de pré-condições, pós-condições, e invariantes. Como exemplo de linguagem de especificação por contrato tem-se Java Modeling Language (JML) específica para programas Java. Apesar de a especificação formal melhorar a confiabilidade do software, deve-se haver certificação de que a implementação está em conformidade com a especificação definida. Verificação de conformidade em programas com contratos é geralmente realizada através de análises manuais ou verificação dinâmica, e em fases tardias do processo de desenvolvimento do software, ou seja, quando o produto final encontra-se disponível para o cliente. Nesta situação, o tempo despendido para detectar não-conformidades pode ser muito longo, ocasionando, consequentemente, atrasos no cronograma e aumento nos custos. Neste trabalho, propomos uma abordagem para checar conformidade entre código fonte e especificação formal por contratos através da geração e execução de testes. Testes de unidade são gerados automaticamente, resultando em casos de testes com sequências de chamadas aos métodos e construtores. Os contratos são transformados em assertivas que funcionam como oráculo para os testes. Esta abordagem não garante corretude total do software, mas aumenta a confiança quando uma não-conformidade é encontrada e, além disso, encoraja o uso de especificação por contratos. Nós implementamos JMLOK, uma ferramenta que executa os passos desta abordagem automaticamente no contexto de programas Java especificados com Java Modeling Language (JML). JMLOK foi avaliada em grupos de programas Java/JML, incluindo um módulo do projeto JavaCard. Todas as unidades experimentais totalizam 18 KLOC e 5K de linhas de especificação JML. Todo o processo consumiu menos que 10 minutos de execução e gerou como resultado a detecção de 29 não-conformidades. As causas das ocorrências das não-conformidades foram analisadas manualmente e classificadas em categorias de falhas. / Writing formal specifications by contracts is a practical and reliable way to build softwares in which developers and clients keep an agreement with rights and obligations to be fulfilled. These responsibilities are expressed basically by pre-conditions, post-conditions and invariants. As example of specification language by contract there is Java Modeling Language (JML) that is specific to Java programs. Although formal specification improves software rehabihty, it should exist certification of conformance with defined specification. Verify conformance between programs and contracts is usually performed by manual analysis or dynamic verification, and in late stages of software development process, that is, when the final product is available to client. In this situation, the time required to detect nonconformances could be so long, causing, consequently, schedule delays and increased costs. In this work, we propose an approach to check conformance between source code and contract formal specification through testing generation and execution. Unit tests are generated automatically resulting in test cases with call sequences of methods and constructors. The contracts are translated in assertions that work like test oracle. We have implemented JMLOK, a tool performs the approach steps automatically in the context of Java programs specified with Java Modeling Language (JML). JMLOK was evaluated in Java/JML programs groups, including a module of the JavaCard project. All the experimental units totalize 18 KLOC and 5K lines of JML specification. All process took less than 10 minutes of running and generated as result 29 nonconformances. The causes of nonconformances occurring were analyzed manually and classified in categories of fails.