An extension of a tool for the formal support for component-based development

• Ano de defesa: 2017
• Autor(a) principal: Pereira, Dalay Israel de Almeida
• Orientador(a): Oliveira, Marcel Vinicius Medeiros
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Programa de Pós-Graduação: PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO
• País: Brasil
• Palavras-chave em Português: Sistemas baseados em componentes; CSP; Automação; SMT; Deadlock; Ferramenta; Extensão
• Área do conhecimento CNPq: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO
• Link de acesso: https://repositorio.ufrn.br/jspui/handle/123456789/24200

Utilizando a abordagem de desenvolvimento baseado em componentes, a complexidade dos sistemas é reduzida e a sua manutenção é facilitada, trazendo mais segurança e reuso dos componentes. Porém, a composição dos componentes (e suas interações) ainda é uma grande fonte de problemas e requer uma análise mais detalhada. Esse problema é ainda mais relevante quando lidamos com aplicações críticas. Uma abordagem para especificar esse tipo de aplicação é o uso de Métodos Formais, uma metodologia precisa para a especificação de sistemas, que possui uma base matemática forte e que traz, entre outros benefícios, mais segurança. Como exemplo, o método formal CSP permite a especificação de sistemas concorrentes e a verificação de propriedades inerentes a esses sistemas. CSP dispõe de um conjunto de ferramentas para a sua verificação, como, por exemplo, FDR. Usando CSP é possível indentificar e resolver problemas como deadlock e livelock em um sistema, muito embora isso possa ser custoso em termos de tempo gasto em verificações. Nesse contexto, BRIC surge como uma abordagem baseada em CSP para o desenvolvimento de sistemas baseados em componentes, garantindo a ausência de deadlock e livelock por construção. Essa abordagem usa CSP para especificar restrições e interações entre componentes de maneira a permitir uma verificação formal do sistema. Uma extensão de BRIC, BRICK , propõe adicionar metadados aos componentes a fim de diminuir a complexidade e a quantidade das verificações feitas quando componentes são compostos. Porém, a aplicação prática dessa abordagem pode se tornar muito complexa e cansativa se feita manualmente. Com o objetivo de automatizar o uso da abordagem BRICK , foi desenvolvida anteriormente uma ferramenta (BTS - BRICK Tool Support) que automatiza as verificações das composições dos componentes gerando e verificando automaticamente as condições impostas pela abordagem utilizando FDR. Porém, devido ao número e à complexidade das verificações feitas em FDR, a ferramenta pode levar ainda muito tempo nesse processo. Esta dissertação apresenta uma extensão à BTS que melhora o modo como são feitas as verificações, substituindo o FDR utilizado na ferramenta pela sua mais recente versão e adicionando um provador SMT que, concorrentemente, verifica algumas das propriedades da aplicação. Nós também adaptamos a ferramenta para ser usada na especificação de um maior número de sistemas e avaliamos a ferramenta estendida com dois estudos de caso, comparando as verificações feitas na versão anterior da ferramenta com a nossa nova abordagem de verificação.