Sistemas baseados em componentes, CSP, Automação, SMT, Deadlock

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.