Ir para o conteúdo. | Ir para a navegação

Ferramentas Pessoais
Acessar
Seções
Você está aqui: Página Inicial

Verites - Verificação, Validação e Teste de Software

Grupo de Validação, Verificação e Teste

Página do Grupo de Validação, Verificação e Teste do Instituto de Informática da UFRGS.

***************************************

Suplementary files for article

"Use case evolution based on graph transformation"

submitted to ICSE 2017 are available here

***************************************

Motivação e Objetivos

Atualmente muitas atividades importantes são desempenhadas por componentes de software. Como exemplo, podemos citar a compra de passagens aéreas e a utilização de serviços bancários via Internet. Devido à essa utilização em larga escala de software e à sua crescente complexidade, muitos esforços têm sido colocados no desenvolvimento de técnicas para melhor detectar e corrigir erros no seu desenvolvimento, e, dessa forma, aumentar a confiabilidade de tais sistemas. Essas garantias são particularmente relevantes quando lidamos com sistemas onde erros possam levar a prejuízos financeiros significativos (como sistemas bancários) ou pôr em risco a vida das pessoas (como sistemas de controle em veículos automotores).

O Grupo de Validação, Verificação e Teste de Sistema Computacionais pesquisa métodos cujo o propósito é a melhoria da qualidade de software. Como exemplo, podemos citar:

  • Critérios para construção de testes e metodologias para sua aplicação
  • Modelos para a representação formal do sistema, sobre os quais podemos aplicar técnicas como
    • Construção de provas de correção utilizando assistentes de prova (semi-automatizado)
    • Verificação de modelos (automatizado)
  • Formas de automatizar ou simplificar a construção de modelos de software
  • Novas técnicas de análise sobre linguagens de programação ou modelos de software
  • Desenvolvimento de novas ferramentas para validação e verificação de software

 

Tópicos de Pesquisa (atuais)

  • Extração de modelos: O uso de modelos para validação e verificação de sistemas, dentro do ciclo de desenvolvimento, tem sido de grande valia e oportunizado a descoberta de erros graves mesmo antes dos sistemas entrarem em atividade. No entanto, a construção de um modelo e a posterior implementação baseada neste modelo são geralmente processos não triviais, especialmente para sistemas complexos, onde erros podem estar mais bem ocultos e são mais difíceis de serem detectados. Por isto, abordagens de extração de modelos provêm a possibilidade de construção de modelos a partir de implementações existentes. Se o modelo corresponde fielmente ao que foi implementado, análises sobre o modelo correspondem a análises sobre o sistema, só que o modelo é mais abstrato e, por isso, mas fácil de lidar. Além disso, como o modelo é gerado do código, alterações no código podem ser facilmente repassadas ao modelo, dando suporte à evolução e mantendo a consistência entre modelo e implementação. Seguindo esta ideia, desenvolvemos pesquisas em torno de como melhorar o suporte atual para extração de modelos e análises que podem ser feitas sobre os modelos extraídos.
  • Evolução de sistemas: Sistemas computacionais evoluem, sendo que esta evolução pode criar, remover ou preservar certos comportamentos do sistema. Neste contexto, definimos um modelo denominado gramática de grafos de segunda ordem que permite rastrear e descrever evoluções sobre um modelo de software, e estudamos técnicas de análise para estudar o efeito da evolução sobre a semântica original do sistema.
  • Correção de sistemas utilizando assistentes de prova e verificação de modelos: determinar se um sistema satisfaz uma certa propriedade é habitualmente um problema complexo, muitas vezes indecidível. Há duas abordagens principais: verificação de modelos e assistentes de prova. Verificadores de modelo são sistemas que recebem um modelo de software e uma propriedade a ser verificada, determinando de forma automática se a propriedade é satisfeita pelo modelo. Verificadores de modelos habitualmente assumem que o modelo de entrada é finito, e requerem algoritmos e estruturas de dados sofisticados para evitar o problema de explosão do espaço de estado. Assistentes de prova são ferramentas que permitem expressar provas matemáticas, sendo úteis para garantir a correção das mesmas. Provadores habitualmente permitem a descrição de objetos matemáticos complexos tais como modelos de software, assim como a descrição de propriedades sobre esses modelos. Ao contrário de verificação de modelos, a construção das provas ou determinação de contraexemplos para propriedades não é completamente automatizado em assistentes de provas, embora possa ser auxiliado através de táticas programáveis. Em contrapartida, assistentes de prova permitem a verificação de propriedades estruturais de estruturas infinitas.
  • Formalização, análise e melhoramento de Casos de Uso:Metodologia para a geração de modelos para representar comportamentos descritos em Casos de Uso, os quais descrevem situações de utilização de um software e são usados para documentar este software na etapa de projeto. Os modelos criados servem de entrada para ferramentas onde é possível realizarem-se diversas análises com o intuito de identificação erros tais como inconsistências, omissões e conflitos. A identificação destes problemas permite que os Casos de Uso originais sejam corrigidos/melhorados. Se o sistema ainda estiver na etapa de projeto, a descoberta destes erros reduz o custo de futuras manutenções e melhora a documentação do software para a implementação. Caso o sistema já esteja implementado, os erros detectados podem servir para a criação de casos de teste a fim de verificar se a implementação possui estes erros, levando a uma posterior correção dos mesmos. A metodologia proposta inclui níveis de severidade dos erros, que servem para a tomada de decisão sobre quais devem ser considerados com mais cuidado e quais podem ser decorrentes apenas de decisões de projeto.

Temas para Trabalhos de Conclusão, Dissertações e Teses

Trabalhos de Conclusão de Curso

  • Interface AGG para lidar com hierarquia de gramáticas
  • Interface AGG para integrar descrição de Use Cases e a ferramenta de geração de gramáticas
  • Geração automatizada de testes a partir de artefatos de projeto UML
  • Interface gráfica para edição de gramáticas de grafos (Haskell)
  • Implementação de atributos em grafos, regras e gramáticas (Haskell)
  • Análise de conformidade de modelos de comportamento
  • Criação de interfaces gráficas para ferramentas de VV&T
  • Combinação de Teste e Verificação Formal
  • Instrumentação de código
  • Extração de modelos probabilísticos
  • Implementação de estudos de caso
  • Aplicações de verificação de modelos e análise estática

Dissertações de Mestrado

  • Extração de gramática de grafos a partir de código Java
  • Extração de gramática de grafos a partir de artefatos de projeto UML (diagrama de classes e diagrama de interação)
  • Geração de testes a partir de gramática de grafos
  • Estudo de técnicas de equivalência entre gramáticas
  • Estudo de técnicas de refinamento de gramáticas
  • Estudo de refinamento automático de modelos de comportamento
  • Extração de modelos de sistemas embarcados
  • Specification mining

Teses de Doutorado

  • Evolução de gramáticas e preservação de propriedades
  • Aplicação da noção de transação no contexto de Use Cases e outros artefatos de projeto UML
  • Geração de testes a partir de transações
  • Framework para extração e análise de modelos de comportamento


Nota (para Trabalhos de graduação e Mestrado): embora lidem com aspectos teóricos da computação como modelos e análises formais, os trabalhos propostos nesta linha tem também caráter bastante prático pois envolvem implementação de ferramentas de apoio ao desenvolvimento e à análise formal. Os trabalhos propostos buscam justamente aproximar técnicas de análise às metodologias de desenvolvimento de software atuais. Neste sentido, o aluno poderá fortalecer seus conhecimentos tanto teóricos como práticos.

Projetos

  • Uma Metodologia para o Desenvolvimento de Software Confiável por Construção (finalizado)
  • VeriTes - Verificação e Teste de Sistemas Computacionais (em andamento)

 

Apoio

  1. CNPq
  2. FAPERGS

 

Pesquisadores

Professores membros

Colaboradores externos

Alunos

  • Andrei Costa (Pós-Graduação - Mestrado). Orientadora: Leila Ribeiro
  • Guilherme Grochau Azzi (Pós-Graduação - Mestrado). Orientadora: Leila Ribeiro
  • Jonas Santos Bezerra (Pós-Graduação - Mestrado). Orientadora: Leila Ribeiro
  • Leonardo Marques Rodrigues (Graduação - IC). Orientador: Rodrigo Machado
  • Thiago Rafael Becker (Graduação - IC). Orientador: Rodrigo Machado
  • Ricardo Gabriel Herdt (Graduação - IC). Orientador: Rodrigo Machado
  • Eduardo Correa Both (Graduação - IC). Orientador: Lucio Mauro Duarte (trabalho finalizado)
  • Marcos Antônio de Oliveira Júnior (Pós-Graduação - Mestrado). Orientadora: Leila Ribeiro
  • Clei Souza Júnior (Graduação - IC). Orientador: Lucio Mauro Duarte (trabalho finalizado)

Publicações

  • Dotti, F. L.; Duarte, L. M.; Foss, L.; Ribeiro, L.; Russi, D. & dos Santos, O. M. "An Environment for the Development of Concurrent Object-Based Applications". Electronic Notes on Theoretical Computer Science, Elsevier Science Publishers B. V., 2005, 127, 3-13.
  • Duarte, L. M.; Kramer, J. & Uchitel, S. "Model Extraction Using Context Information". Model Driven Engineering Languages and Systems, Springer Berlin Heidelberg, 2006, LNCS 4199, 380-394.
  • Duarte, L.; Kramer, J. & Uchitel, S. "Towards Faithful Model Extraction Based on Contexts". Fundamental Approaches to Software Engineering, Springer Berlin Heidelberg, 2008, LNCS 4961, 101-115.
  • Duarte, L.; Foss, L.; Wagner, F. & Heimfarth, T. "A Probabilistic Model Checking Technique for the Verification of Self-Organising Emergent Systems". Anais do XXXVII Seminário Integrado de Software e Hardware (SEMISH), SBC, 2010.
  • Duarte, L.; Foss, L.; Wagner, F. & Heimfarth, T. et al. "Model Checking the Ant Colony Optimisation". DIPES/BICC 2010, Springer, 2010, 329, 221-232.
  • Duarte, L. "Integrating Software Testing and Model Checking Through Model Extraction". 14th Brazilian Symposium on Formal Methods (SBMF) : short papers, 2011, 73-78.

Notícias

Notícias deste site
Notícias
Notícias deste site

Imagens

Image Logo
Logo