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!
|
| Resumo: | 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. |
|---|