English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de Dissertação de Mestrado N° 1668 "Um Verificador de Modelos para Circus em K"

O aluno Fabio Soares dos Santos irá defender sua pesquisa no dia 15 de setembro, às 8h, no Anfiteatro do CIn-UFPE Início: 15/09/2016 às 08:00 Término: 15/09/2016 às 00:00 Local: Anfiteatro do CIn

 Pós-Graduação em Ciência da Computação – UFPE

Defesa de Dissertação de Mestrado Nº 1.668

Aluno: Fabio Soares dos Santos
Orientador: Prof. Alexandre Cabral Mota
Co-orientador: Prof. Adalberto Cajueiro de Farias (DSC/UFCG)
Título: Um Verificador de Modelos para Circus em K
Data: 15/09/2016
Hora/Local: 8h – Centro de Informática  – Anfiteatro
Banca Examinadora:
Prof. Augusto Cezar Alves Sampaio (UFPE / CIn)
Prof. Sidney de Carvalho Nogueira  (UFRPE / DEINFO)
Prof. Alexandre Cabral Mota  (UFPE / CIn)


RESUMO:

Testes constituem uma parcela significativa da energia despendida em projetos voltados ao desenvolvimento de softwares. Estima-se que entre 30% a 50% do custo total do projeto é destinado a testes. Esta necessidade de verificar a regularidade de sistemas é bastante antiga e nos últimos anos a busca por novas técnicas e ferramentas que mitiguem o esforço gasto nestas verificações vem se acentuando. Neste contexto, uma técnica que se destaca é a de verificação de modelos (Model checking) que consiste em explorar exaustivamente todos os estados alcançáveis de um determinado sistema no intuito de descrever cenários
que indiquem possíveis comportamentos, embasando tal verificação em matemática precisa e inequívoca. Esta técnica tem despertado o interesse de muitas indústrias devido ao sucesso obtido pelo apoio das ferramentas de verificação de modelos (Model checkers) em vários projetos de alta complexidade. Estes verificadores são ferramentas que exploram um sistema de transições rotuladas (LTS), construído a partir de algumas especificações (um modelo M), para determinar se uma dada fórmula (f) lógica temporal, ou propriedade, é válida; ou simplesmente, M |= f. O presente trabalho apresentará uma forma intuitiva e sistemática de construir um verificador de modelos LTL para a linguagem Circus totalmente baseado na semântica operacionais desta linguagem. Mas em vez de codificar diretamente o verificador de modelos com alguma linguagem de programação, será usado o K framework
por se tratar de um framework semântico executável à base de reescrita em que as linguagens de programação, sistemas de tipos e ferramentas de análise formais podem ser definidos usando configurações, computações e regras. Além disso, a ferramenta resultante deste trabalho será demostrada com alguns casos de estudos no intuito de comparar seu desempenho com outros verificadores de modelos.

Palavras-chave: Circus, Verificador de modelos, Análise, K-Framework, Semântica operacional, SMT.

  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web