An extension of a tool for the formal support for component-based development
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 det...
Na minha lista:
| Autor principal: | |
|---|---|
| Outros Autores: | |
| Formato: | Dissertação |
| Idioma: | por |
| Publicado em: |
Brasil
|
| Assuntos: | |
| Endereço do item: | https://repositorio.ufrn.br/jspui/handle/123456789/24200 |
| Tags: |
Adicionar Tag
Sem tags, seja o primeiro a adicionar uma tag!
|
| id |
ri-123456789-24200 |
|---|---|
| record_format |
dspace |
| institution |
Repositório Institucional |
| collection |
RI - UFRN |
| language |
por |
| topic |
Sistemas baseados em componentes CSP Automação SMT Deadlock Ferramenta Extensão CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO |
| spellingShingle |
Sistemas baseados em componentes CSP Automação SMT Deadlock Ferramenta Extensão CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO Pereira, Dalay Israel de Almeida An extension of a tool for the formal support for component-based development |
| description |
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. |
| author2 |
Oliveira, Marcel Vinicius Medeiros |
| author_facet |
Oliveira, Marcel Vinicius Medeiros Pereira, Dalay Israel de Almeida |
| format |
masterThesis |
| author |
Pereira, Dalay Israel de Almeida |
| author_sort |
Pereira, Dalay Israel de Almeida |
| title |
An extension of a tool for the formal support for component-based development |
| title_short |
An extension of a tool for the formal support for component-based development |
| title_full |
An extension of a tool for the formal support for component-based development |
| title_fullStr |
An extension of a tool for the formal support for component-based development |
| title_full_unstemmed |
An extension of a tool for the formal support for component-based development |
| title_sort |
extension of a tool for the formal support for component-based development |
| publisher |
Brasil |
| publishDate |
2017 |
| url |
https://repositorio.ufrn.br/jspui/handle/123456789/24200 |
| work_keys_str_mv |
AT pereiradalayisraeldealmeida anextensionofatoolfortheformalsupportforcomponentbaseddevelopment AT pereiradalayisraeldealmeida extensionofatoolfortheformalsupportforcomponentbaseddevelopment |
| _version_ |
1773958686693130240 |
| spelling |
ri-123456789-242002022-04-11T21:55:48Z An extension of a tool for the formal support for component-based development Pereira, Dalay Israel de Almeida Oliveira, Marcel Vinicius Medeiros http://lattes.cnpq.br/4599023777376618 http://lattes.cnpq.br/1756952696097255 http://lattes.cnpq.br/1756952696097255 Sampaio, Augusto Cezar Alves http://lattes.cnpq.br/3977760354511853 Musicante, Martin Alejandro http://lattes.cnpq.br/6034405930958244 Sistemas baseados em componentes CSP Automação SMT Deadlock Ferramenta Extensão CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAO 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. 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. 2017-11-07T19:51:30Z 2017-11-07T19:51:30Z 2017-08-18 masterThesis PEREIRA, Dalay Israel de Almeida. An extension of a tool for the formal support for component-based development. 2017. 83f. Dissertação (Mestrado em Sistemas e Computação) - Centro de Ciências Exatas e da Terra, Universidade Federal do Rio Grande do Norte, Natal, 2017. https://repositorio.ufrn.br/jspui/handle/123456789/24200 por Acesso Aberto application/pdf Brasil UFRN PROGRAMA DE PÓS-GRADUAÇÃO EM SISTEMAS E COMPUTAÇÃO |