Banca de QUALIFICAÇÃO: MADIEL DE SOUZA CONSERVA FILHO

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE: MADIEL DE SOUZA CONSERVA FILHO
DATA: 11/12/2015
HORA: 10:00
LOCAL: CIVT/IMD - Sala A305
TÍTULO:

Livelock Analysis for Component-Based Systems


PALAVRAS-CHAVES:

Engenharia de Software, Métodos Formais, Concorrência, Desenvolvimento Baseados em Componentes, Divergência


PÁGINAS: 100
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:

O uso crescente de sistemas complexos exige cada vez mais um maior investimento de recursos no desenvolvimento de software para garantir a confiabilidade dos sistemas. Para lidar com esta complexidade, abordagens composicionais podem ser utilizadas no desenvolvimento de sistemas de software, possibilitando a integração e a reutilização de componentes existentes. Entretanto, a fim de garantir o sucesso desta abordagem, é essencial confiar no comportamento dos componentes e, além disso, nos sistemas que são desenvolvidos utilizando essa estratégia. Problemas podem surgir quando dois ou mais componentes são integrados pela primeira vez. Este problema é ainda mais relevante quando um grupo de componentes trabalha em conjunto a fim de executar determinadas tarefas, especialmente em sistemas concorrentes, durante o qual podem surgir problemas clássicos, como livelock. Nesta proposta de tese de doutorado, nós propomos uma estratégia local para garantir ausência de divergência, por construção, em sistemas síncronos modelados com a notação padrão de CSP. Além disto, a abordagem proposta pode ser aplicada para verificar ausência de livelock em modelos que realizam comunicações assíncronas. Neste caso, nós analisamos o modelo de componente BRIC, cujo comportamento dos componentes é representado por um processo CSP. Neste contexto, nós também propomos uma abordagem correta por construção a fim de assegurar composições BRIC livres de livelock, realizando uma verificação local. A abordagem foi avaliada através de três estudos de caso: milner e duas variações do jantar dos filósofos, uma versão representa um sistema livre de livelock, e a outra inclui um sistema com livelock. Nós realizamos uma análise comparativa destes estudos de caso em três diferentes abordagens: (1) a tradicional análise global do FDR, (2) a análise estática de livelock do SLAP, (3) e a nossa estratégia local e composicional de livelock.


MEMBROS DA BANCA:
Externo à Instituição - ALEXANDRE CABRAL MOTA - UFPE
Interno - 1258224 - ANAMARIA MARTINS MOREIRA
Externo à Instituição - AUGUSTO CEZAR ALVES SAMPAIO - UFPE
Presidente - 1639701 - MARCEL VINÍCIUS MEDEIROS OLIVEIRA
Notícia cadastrada em: 08/12/2015 16:40
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa01-producao.info.ufrn.br.sigaa01-producao