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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/24200 |
| Date | 18 August 2017 |
| Creators | Pereira, Dalay Israel de Almeida |
| Contributors | 02386943488, Sampaio, Augusto Cezar Alves, 41521633487, Musicante, Martin Alejandro, 82500304434, Oliveira, Marcel Vinicius Medeiros |
| Publisher | PROGRAMA DE P?S-GRADUA??O EM SISTEMAS E COMPUTA??O, UFRN, Brasil |
| Source Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | English |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0023 seconds