English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de Tese de Doutorado Nº 370: "Validating Transformations of Programs using the Alloy Analyzer"

A aluna Tarciana Dias da Silva irá defender sua tese no dia 23 de agosto, às 8h30, no Auditório Início: 23/08/2017 às 14:00 Término: 23/08/2017 às 16:00 Local: Auditório do CIn

Pós-Graduação em Ciência da Computação – UFPE
Defesa de Tese de Doutorado Nº  370

Aluno: Tarciana Dias da Silva
Orientador: Prof.. Augusto Cézar Alves  Sampaio
Co-orientador: Prof. Alexandre Cabral Mota
Título: Validating Transformations of Programs using the Alloy Analyzer
Data: 23/08/2017
Hora/Local: 8h30 – Centro de Informática - Auditório
Banca Examinadora:
Prof. Márcio Lopes Cornélio  (UFPE / Centro de Informática)
Prof. Juliano Manabu Iyoda  (UFPE / Centro de Informática)
Prof. Leopoldo Motta Teixeira  (UFPE / Centro de Informática)
Prof. Rohit Gheyi  (UFCG / Departamento de Sistemas e Computação)
Prof. Ana Cristina Vieira de Melo  (USP / Instituto de Matemática e Estatística)


RESUMO:

Transformações de programas é uma prática atual em desenvolvimento de software, especialmente refactoring. No entanto, em geral, não há uma especificação precisa dessas transformações e, quando existe, não é provada correta nem sistematicamente validada, o que pode causar erros de semântica estática ou comportamentais nos programas resultantes da transformação. Este trabalho propõe uma estratégia, baseada numa infraestrutura formal construída predominantemente em Alloy, para validar especificações de transformação de programas. Neste trabalho, nós focamos em transformaçõoes em linguagens que suportam características OO tais como Java [28, 7], ROOL [6], leis de refinamento no cálculo de refinamento de componentes e sistemas orientados a objetos, conhecido como rCOS [26] e em uma linguagem OO com semântica de referência descrita em [25]. Nosso foco atual, com relação à implementação da estratégia, é um subconjunto de Java. Complementarmente a testes, linguagens formais fornecem um mecanismo de raciocínio matematicamente sólido para estabelecer a consistência (soundness) das transformaçõoes. Infelizmente, um tratamento formal completo para transformações em linguagens OO é descartado porque, mesmo para Java, não há uma semântica formal completa. Nós
investigamos a veracidade de transformações de programas usando uma abordagem que combina (bounded) model finding e testes. A entrada para nossa estratégia são especificações de transformações de programas descritos numa variedade de notações incluindo um estilo algébrico de apresentação (representado por uma lei algébrica ou regra de refatoramento), ou em notações de modelos de componentes como rCOS. No caso da uma notação algébrica, cada especificação de transformação pretende expressar uma equivalência semântica entre os programas inicial (SS) e resultante (RS), após a transformação. Nossa infra–estrutura formal Alloy é composta de quatro modelos Alloy principais:
(1) um metamodelo para um subconjunto de características de linguagens OO e um conjunto de predicados que capturam a semântica estática correspondente, onde o predicado principal é capaz de determinar se um programa é bem–formado; (2) um modelo específico para cada transformação (que está sendo investigada); (3) um Validador de Semântica Estática, que procura (se existir) por instâncias geradas pela transformação, dos programas resultantes, com problemas de semântica estática; e (4) um Validador
Dinâmico, que gera instâncias possíveis da transformação (de acordo com o escopo especificado), cada uma tendo uma representação de um programa antes e depois da transformação. Se quaisquer instâncias são geradas em (3), isto significa que há uma falha (de semântica estática) na especificação da transformação. Neste caso, é necessário corrigir a especificação e re–submetê–la para o Alloy Analyzer. Este procedimento é repetido até nenhuma instância ser encontrada pelo modelo do Validador de Semântica Estática. Logo, as instâncias geradas pelo modelo do Validador Dinâmico (4) tipicamente somente
representam programas bem formados já que este é aplicado na nossa estratégia apenas
depois que o modelo em (3) não retornar instância alguma. Em seguida, as instâncias
geradas em (4) são submetidas a uma ferramenta, denominada Tradutor de Alloy para Java (Alloy–To–Java Translator), que transforma as instâncias geradas dos pares de
programas em (4) em programas Java. Java é a linguagem escolhida para ilustrar a
estratégia proposta já que sua semântica (pelo menos o subconjunto necessário para
avaliar as transformações) é semelhante às das linguagens nas quais as transformações
foram especificadas. Estes programas são finalmente validados com relação a problemas
de semântica dinâmica. Para isso, testes gerados de forma simplificada são utilizados, em
que as chamadas aos métodos em comum de cada classe são geradas de maneira aleatório
e os resultados comparados estruturalmente.
Dessa forma, um desenvolvedor pode implementar as transformações com alguma
segurança em relação à preservação de comportamento depois de validar a especificação
das transformações usando o framework proposto. A estratégia que propomos parece
promissora já que é uma alternativa para validar transformações em geral (e talvez provar
formalmente a correturde de tais transformações) mesmo quando uma semântica completa
da linguagem não está disponível. Resultados da validação de um conjunto representativo
de refactorings, encontrados na literatura, mostram que alguns problemas de transformações
podem ser detectados, evitando o esforço para implementá–las numa linguagem
fonte e subsequentemente submetê–las a uma campanha de testes mais elaborada.

Palavras-chave: Java, Transformações de Programas, Alloy, Validação
  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web