Defesa de dissertação de Catuxe Varjão 15/3

postado em 24 de mai de 2013 08:00 por Nazareno Ferreira de Andrade   [ 24 de mai de 2013 08:14 atualizado‎(s)‎ ]
Candidato: Catuxe Varjão
Título do trabalho: Uma Abordagem para Verificar Não-conformidades em Programas Especificados com Contratos
Orientador(es): Tiago Massoni Rohit Gheyi

Data: 15/03/2013
Local: Auditório do CEEI

Banca examinadora: Márcio Lopes Cornélio (UFPE), Adalberto Cajueiro (UFCG). 

Resumo: Especificar formalmente módulos de programas, tais como classes e interfaces, tendem a melhorar a qualidade do software. A escrita de especificações formais por contratos é uma maneira confiável e prática de construir softwares, em que desenvolvedores e clientes man- têm um acordo contendo direitos e obrigações a serem cumpridos. Essas responsabilidades são expressas basicamente através de asserções do tipo pré-condições (restrições a serem cumpridas pelo cliente), pós-condições (restrições a serem cumpridas pelos desenvolvedores dos módulos), e invariantes (restrições a serem cumpridas tanto por clientes quanto por de- senvolvedores). 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 for- mal melhorar a confiabilidade do software, deve-se haver certificação de que a implemen- taçã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 e sua im- plementação (JMLOK) para checar conformidade entre código fonte e especificação formal por contratos através da geração e execução de 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), através da geração au- tomática e aleatória de testes de unidade. JMLOK foi avaliada em pequenos exemplos e em programas reais, incluindo um módulo do projeto JavaCard massivamente especificado com cláusulas JML. JMLOK foi avaliado em 16 KLOC e 5000 linhas de especificação JML, o que consumiu menos que 10 minutos de execução e gerou como resultado a detecção de 23 não-conformidades.
Comments