Banca de DEFESA: MADIEL DE SOUZA CONSERVA FILHO

Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DISCENTE : MADIEL DE SOUZA CONSERVA FILHO
DATA : 12/08/2016
HORA: 09:00
LOCAL: IMD/CIVT Sala B321
TÍTULO:

Livelock Analysis for Component-Based Systems


PALAVRAS-CHAVES:

Component-based systems; Formal Methods; Livelock Freedom, Local Analysis.


PÁGINAS: 150
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 use of increasingly complex applications is demanding a greater investment of
resources in software development to ensure that applications are safe. For mastering
this complexity, compositional approaches can be used in the development of software
by integrating and reusing existing reliable components. The correct application of such
strategies, however, relies on the trust in the behaviour of the components and in the emergent
behaviour of the composed components because failures may arise if the composition
does not preserve essential properties. Problems may be introduced when two or more
error-free components are integrated for the first time. This concern is even more relevant
when a group of components is put together in order to perform certain tasks, especially in
safety-critical applications, during which classical problems can arise, such as livelock.
In this thesis, we present the development of a local strategy that guarantees, by
construction, the absence of livelock in synchronous systems as modelled using the
standard CSP notation. Our method is based solely on the local analysis of the minimum
sequences that lead the CSP model back to its initial state. Locality provides an alternative
to circumvent the state explosion generated by the interaction of components and allows us
to identify livelock before composition. The verification of these conditions use metadata
that allow us to record partial results of verification, decreasing the overall analysis effort.
In addition, our work can also be applied to check livelock freedom in models that perform
asynchronous communications. In this case, we carry out livelock analysis in the context
of a component model, BRIC, whose behaviour of the components is described as a CSP
process. Finally, we introduce three case studies to evaluate the our livelock-analysis
technique in practice: the Milner’s scheduler and two variations of the dining philosophers,
a livelock-free version and a version in which we have deliberately included livelock. For
each case study, we also present a comparative analysis of the performance of our strategy
with two other techniques for livelock freedom verification, the traditional global analysis
of FDR and the static livelock analysis of SLAP. This comparative study demonstrates that
our strategy can be used in practice and that it might be a useful alternative for establishing
livelock freedom in large systems.


MEMBROS DA BANCA:
Interno - 1258224 - ANAMARIA MARTINS MOREIRA
Interno - 1639701 - MARCEL VINÍCIUS MEDEIROS OLIVEIRA
Interno - 1221251 - MARTIN ALEJANDRO MUSICANTE
Externo à Instituição - ALEXANDRE CABRAL MOTA - UFPE
Externo à Instituição - LEILA RIBEIRO - UFRGS
Notícia cadastrada em: 06/07/2016 00:23
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa04-producao.info.ufrn.br.sigaa04-producao