Banca de QUALIFICAÇÃO: DALAY ISRAEL DE ALMEIDA PEREIRA

Uma banca de QUALIFICAÇÃO de MESTRADO foi cadastrada pelo programa.
DISCENTE : DALAY ISRAEL DE ALMEIDA PEREIRA
DATA : 10/02/2017
HORA: 09:00
LOCAL: Instituto Metrópole Digital - CIVT - Sala B321
TÍTULO:

Uma extensão de uma ferramenta para o suporte formal ao desenvolvimento baseado em componentes


PALAVRAS-CHAVES:
Sistemas baseados em componentes, CSP, Automação, SMT, Deadlock

PÁGINAS: 100
RESUMO:
O desenvolvimento de sistemas baseado em componentes é considerado uma evolução para o processo de desenvolvimento de software. Usando essa abordagem, a manutenção do sistema é facilitada, trazendo mais segurança e reuso. A composição de componentes (e suas interações), entretanto, é ainda a maior fonte de problemas e requer uma análise mais detalhada. Métodos formais são uma ferramenta precisa para a especificação de sistemas e possui uma base matemática forte que traz, entre outros benefícios, mais segurança para os sistemas. O método formal CSP permite a especificação de sistemas concorrentes e a verificação de propriedades inerentes a esses sistemas. CSP tem um conjunto de ferramentas que auxiliam na sua verificação, como FDR2 e FDR3. Porém, a verificação de algumas propriedades podem levar muito tempo, como, por exemplo, a verificação da ausência de deadlock. BRICK surge como uma abordagem baseada em CSP para o desenvolvimento de sistemas assíncronos baseados em componentes que garante a ausência de deadlock por construção. Essa abordagem usa CSP para especificar constantes e interações entre os componentes a fim de permitir uma verificação do sistema em si. Entretanto, o uso prático dessa abordagem pode ser muito complexo e cansativo. A fim de automatizar o uso de BRICK nós desenvolvemos uma ferramenta (BTS - BRICK Tool Support) que automatiza a verificação da composição de componentes por, automaticamente, gerar e checar as condições impostas pela abordagem utilizando FDR2. Porém, devido ao grande número e a complexidade das verificações feitas em FDR2, a ferramenta pode levar muito tempo no processo de verificação. Neste trabalho, nós apresentamos uma extensão para BTS que melhora a maneira pela qual a ferramenta faz as verificações, trocando FDR2 para FDR3 e adicionando um provador de SMT que, concorrentemente, checa algumas das propriedades das especificações. Nós também melhoramos os casos de uso para avaliarmos a nossa ferramenta.

MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINÍCIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Externo à Instituição - BRUNO EMERSON GURGEL GOMES - IFRN
Notícia cadastrada em: 24/01/2017 10:09
SIGAA | Superintendência de Informática - (84) 3215-3148 | Copyright © 2006-2017 - UFRN - sigaa03-producao.info.ufrn.br.sigaa03-producao