Agenda de defesas Agenda de defesas

Voltar

Ciência da Computação promove defesa de dissertação na terça-feira (17)

Defesa ocorrerá na terça-feira (17), às 9h, no auditório do Centro de Informática (CIn)

O Programa de Pós-Graduação em Ciência da Computação (PGCC) irá promover a defesa de dissertação de mestrado “A strategy for local analysis of determinism”, do aluno Rodrigo Benedito Otoni. A defesa ocorrerá na terça-feira (17), às 9h, no auditório do Centro de Informática (CIn).

A banca examinadora é composta pelos professores Alexandre Cabral Mota (UFPE), Augusto Cezar Alves Sampaio (UFPE), Rohit Gheyi (UFCG) e pelo orientador do trabalho, Augusto Cezar Alves Sampaio (UFPE).

Resumo

Não determinismo é um constituinte inevitável de qualquer teoria que descreva concorrência. Para a validação e verificação de sistemas concorrentes, é essencial que se investigue a presença ou a ausência de não determinismo, tanto quanto de outras propriedades, como deadlock e livelock. CSP é uma álgebra de processos bem estabelecida e que oferece ricos modelos semânticos, capazes de capturar uma grande variedade de fontes de não determinismo. A abordagem utilizada pela principal ferramenta de CSP, o verificador de modelos FDR, é verificar determinismo através de uma análise global, o que limita a sua escalabilidade. Nesta dissertação nós propomos uma estratégia de análise local de determinismo para especificações escritas em um subconjunto de CSP. Nosso objetivo é prover um método eficiente e escalável de verificação de determinismo. Nós usamos uma abordagem composicional, partindo de processos determinísticos básicos, e verificando se quaisquer operadores de composição usados na especificação podem introduzir não determinismo. O uso de subconjuntos controlados de certas notações é comum em estratégias de análise local, sendo que o subconjunto de CSP capturado por nossa estratégia contêm os principais operadores de CSP, possibilitando a modelagem de sistemas reais. Além disso, a nossa estratégia é correta, mas não completa; abrir mão de completude é uma decisão comum em estratégias de análise composicional, como uma forma de aumentar a eficiência. Nós apresentamos aqui a nossa estratégia, o protótipo desenvolvido para permitir a sua automação, e os resultados de vários experimentos. Nossa estratégia tem dois elementos principais: os seus metadados, e os seus algoritmos. Após um processo de uma especificação ser verificado como determinístico, nos coletamos metadados sobre ele. Os metadados armazenam todas as informações do processo que são relevantes para a estratégia, sendo o único elemento utilizado nas verificações seguintes. Para cada operador de composição disponível em nosso subconjunto de CSP, nós desenvolvemos um algoritmo específico para verificar se a composição é determinística. Pelo uso dos metadados, nos removemos a necessidade de verificar os operandos a cada composição, o que nos leva a uma abordagem composicional eficiente. Vários estudos de caso foram realizados, nos quais nós comparamos nosso protótipo com FDR. Para a maior parte dos experimentos nosso protótipo e capaz de analisar instanciam que FDR não consegue, devido a falta de memória causada pela explosão de estados. Em alguns casos, nosso protótipo é capaz de analisar instâncias até três ordens de magnitude maiores. Para todas as instâncias nas quais ambas as ferramentas geram um resultado, além das triviais, nosso protótipo é mais eficiente que FDR, com alguns casos em que FDR demora mais que duas horas para chegar a um resultado, e o nosso protótipo requer apenas alguns segundos.

Mais informações
Programa de Pós-Graduação em Ciência da Computação
(81) 2126-8430
secpos@cin.ufpe.br

 

 

Data da última modificação: 12/07/2018, 15:24