Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-11-01T21:17:46Z No. of bitstreams: 1 DalayIsraelDeAlmeidaPereira_DISSERT.pdf: 1298858 bytes, checksum: 8ff640d45df0332e0a20a3f4476198ce (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-11-07T19:51:30Z (GMT) No. of bitstreams: 1 DalayIsraelDeAlmeidaPereira_DISSERT.pdf: 1298858 bytes, checksum: 8ff640d45df0332e0a20a3f4476198ce (MD5) / Made available in DSpace on 2017-11-07T19:51:30Z (GMT). No. of bitstreams: 1 DalayIsraelDeAlmeidaPereira_DISSERT.pdf: 1298858 bytes, checksum: 8ff640d45df0332e0a20a3f4476198ce (MD5) Previous issue date: 2017-08-18 / 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. / Using the component-based development approach, the system complexity is reduced and its maintenance is facilitated, bringing more reliability and reuse of components. However, the composition of components (and their interactions) is still a significant source of problems and requires a more detailed analysis. This problem is even more relevant when dealing with safety-critical applications. An approach for specifying this kind of applications is using Formal Methods, which are a precise methodology for system specification that has strong mathematical background which brings, among other benefits, more safety. As an example, the formal method CSP allows the specification of concurrent systems and the verification of properties inherent to such systems. CSP has a set of tools for verification, like, for instance, FDR. Using CSP, one can detect and solve problems like deadlock and livelock in a system, although it can be costly in terms of the time spent in verifications. In this context, BRICK has emerged as a CSP based approach for developing componentbased systems, which guarantees deadlock and livelock freedom by construction. This approach uses CSP to specify the constraints and interactions between the components to allow a formal verification of the system. An extension to BRIC, BRICK , makes use of metadata as part of the components in order to decrease the complexity and the quantity of verifications made when composing components. However, the practical use of this approach can be too complex and cumbersome. In order to automate the use of the BRICK approach a tool has been previously developed (BTS - BRICK Tool Support), which automates the verifications of component compositions by automatically generating and checking the side conditions imposed by the approach using FDR. Nevertheless, due to the number and complexity of the verifications made in FDR, the tool can still take too much time in this process. In this dissertation, we present an extension to BTS that improves the way how it make verifications by replacing the FDR used inside the tool by its most recent version and adding a SMT-solver, that, concurrently, checks some properties of the specification. We also adapted the tool in order to be used for the specification of a greater number of systems and we evaluated the extended tool with two case studies, comparing the verifications made in the older version of the tool with this new approach of verification.