Banca de DEFESA: DALAY ISRAEL DE ALMEIDA PEREIRA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : DALAY ISRAEL DE ALMEIDA PEREIRA
DATA : 18/08/2017
HORA: 09:00
LOCAL: IMD/CIVT B321
TÍTULO:

An tool extension to formal support to component based development


PALAVRAS-CHAVES:

Component-Based Systems, CSP, Automation, SMT, Deadlock, Tool, Extension.
iv


PÁGINAS: 100
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
RESUMO:

The component-based development of systems is considered an important evolution in the software
development process. Using this approach, the system maintenance is facilitated, bringing
more reliability and reuse of components. However, the composition of components (and their
interactions) is still the main 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 the use Formal Methods, which are an accurate tool
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 its 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 time spent
in verifications. In this context, BRICK has emerged as a CSP based approach for developing
asynchronous component-based systems, which guarantees deadlock freedom by construction.
This approach uses CSP to specify the constraints and interactions between the components to
allow a formal verification of the system. However, the practical use of this approach can be
too complex and cumbersome. In order to automate the use of the BRICK approach we have
developed a tool (BTS - BRICK Tool Support) that automates the verifications of component
compositions by automatically generating and checking the side conditions imposed by the approach
using FDR. But, 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 proposal, 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
evaluated the tool with a new case study, comparing the verifications made in the older version
of the tool with this new approach of verification. The internal structure of the tool has also
been improved in order to make it easier to be extended, which is also an contribution of our
work.


MEMBROS DA BANCA:
Presidente - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Externo à Instituição - AUGUSTO CEZAR ALVES SAMPAIO - UFPE
Notícia cadastrada em: 06/07/2017 17:43
SIGAA | Superintendência de Informática - | | Copyright © 2006-2020 - UFRN - sigaa16-producao.info.ufrn.br.sigaa16-producao