English

CIn - Centro de Informática UFPE




Eventos Relacionados

Defesa de Dissertação de Mestrado Nº 1.382: "A Refinement Based Strategy for Locally Verifying Networks of CSP Processes"

O aluno Pedro Ribeiro Gonçalves Antonino irá defender seu trabalho dia 31 de março, às 8h30, no Auditório Início: 31/03/2014 às 08:30 Término: 31/03/2014 às 10:30 Local: Auditório do CIn

Pós-Graduação em Ciência da Computação – UFPE
Defesa de Dissertação de Mestrado Nº 1.382
 
Aluno: Pedro Ribeiro Gonçalves Antonino
Orientador: Prof. Augusto Cezar Alves Sampaio
Título: A Refinement Based Strategy for Locally Verifying Networks of CSP Processes
Data: 31/03/2013
Hora/Local: 8h30m à Auditório
Banca Examinadora:
Prof. Alexandre Cabral Mota (CIn/UFPE)
Prof. Adalberto Cajueiro de Farias (DSC/UFCG)
Prof. Augusto Cezar Alves Sampaio (CIn / UFPE)
 
RESUMO:
 
Com o aumento da complexidade dos programas, aumentou também a dificuldade da tarefa de verificar se um dado programa atende as expectativas do programador. Nesse caso, métodos formais podem auxiliar no desenvolvimento de programas, fornecendo técnicas para a modelagem e verificação formal de modelos. Essas técnicas auxiliam na construção de modelos dos sistemas, na descrição de propriedades esperadas desses sistemas e na verificação de propriedades dos modelos. No contexto de sistemas concorrentes, a necessidade de uma abordagem formal é ainda mais destacada dada as inumeras possibilidades de interações entre seus sistemas componentes.
Apesar dos benefícios gerados pela integração de métodos formais no processo de desenvolvimento, estes métodos não se encontram completamente aptos a lidar com a complexidade dos sistemas industriais atuais. No caso de sistemas concorrentes a explosão do espaço de estados a ser analisado é o principal fator para essa inéficacia. No contexto de verificação formal, uma das propriedades classicas e esperadas de sistemas concorrentes é a ausencia de deadlocks (impasses). O presente trabalho visa criar uma estratégia formal para a garantia de ausência de deadlocks, que seja capaz de analisar sistemas complexos reais.
Baseado no conceito de redes de processos, o presente trabalho define uma estratégia composicional baseada na verificação automática de propriedades comportamentais que garantem a ausência de deadlocks. A descrição de processos é feita com a notação CSP e a verificação automática dessas propriedades comportamentais, descritas como refinamento de processos, é feita por um verificador de modelos.
 
Palavras-chave: Verificador de modelos, ausência de deadlocks, notação CSP, estratégia composicional. 
  • © Centro de Informática UFPE - Todos os direitos reservados
    Tel +55 81 2126.8430 - Cidade Universitária - 50740-560 - Recife/PE
Plano4 Consultoria Web