Submitted by Automa??o e Estat?stica (sst@bczm.ufrn.br) on 2017-03-09T18:47:46Z
No. of bitstreams: 1
MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) / Approved for entry into archive by Arlan Eloi Leite Silva (eloihistoriador@yahoo.com.br) on 2017-03-10T21:13:38Z (GMT) No. of bitstreams: 1
MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5) / Made available in DSpace on 2017-03-10T21:13:38Z (GMT). No. of bitstreams: 1
MadielDeSouzaConservaFilho_TESE.pdf: 1314650 bytes, checksum: ea38672191d7c35f5274cb1360bcfef1 (MD5)
Previous issue date: 2016-08-12 / O uso crescente de sistemas complexos exige cada vez mais um maior investimento
de recursos no desenvolvimento de software para garantir a confiabilidade dos mesmos.
Para lidar com esta complexidade, abordagens composicionais podem ser utilizadas no
desenvolvimento de sistemas de software, possibilitando a integra??o e a reutiliza??o
de componentes existentes. Entretanto, a fim de garantir o sucesso desta abordagem, ?
essencial confiar no comportamento dos componentes e, al?m disso, nos sistemas que s?o
desenvolvidos utilizando essa estrat?gia, uma vez que falhas podem ser introduzidas se a
composi??o n?o assegurar propriedades importantes. Problemas podem surgir quando dois
ou mais componentes s?o integrados pela primeira vez. Esta situa??o ? ainda mais relevante
quando um grupo de componentes trabalha em conjunto a fim de executar determinadas
tarefas, especialmente em aplica??es cr?ticas, onde podem surgir problemas cl?ssicos, como
livelock. Esta tese de doutorado apresenta uma estrat?gia local para garantir aus?ncia de
livelock, por constru??o, em sistemas s?ncronos modelados com a nota??o padr?o de CSP.
A nossa t?cnica ? baseada na an?lise local das m?nimas sequ?ncias que levam o processo
CSP ao seu estado inicial. O uso de t?cnicas locais evita a explos?o do espa?o de estados
gerado pela integra??o dos componentes. A verifica??o destas condi??es locais utilizam
metadados que permitem armazenar resultados parciais das verifica??es, reduzindo o
esfor?o durante a an?lise. A abordagem proposta tamb?m pode ser aplicada para verificar
aus?ncia de livelock em modelos que realizam comunica??es ass?ncronas. Neste caso,
analisamos o modelo de componentes BR IC, cujo comportamento dos componentes
? representado por um processo CSP. A fim de realizar esta verifica??o, consideramos
duas vers?es para BR IC: BR IC , o qual realiza composi??es ass?ncronas atrav?s de
buffers finitos, e BR IC? no qual a assincronicidade ? realizada atrav?s de buffers infinitos.
Estas duas abordagens foram analisadas porque a possibilidade de introduzir livelock em
sistemas ass?ncronos depende diretamente da finitude do buffer. As t?cnicas propostas para
garantir aus?ncia de livelock em CSP e BR IC foram avaliadas atrav?s de tr?s estudos
de caso: o escalonador de Milner e duas varia??es do jantar dos fil?sofos. Uma vers?o
apresenta um sistema livre de livelock, e a outra apresenta um sistema com livelock. Neste
estudo, avaliamos a nossa abordagem em compara??o com outras duas t?cnicas para
verifica??o de aus?ncia de livelock, a an?lise global tradicional do FDR e a an?lise est?tica
de livelock do SLAP. Este estudo comparativo demonstra que a nossa estrat?gia pode
ser aplicada como uma alternativa para a verifica??o de aus?ncia de livelock em grandes
sistemas. / 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 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, BR IC, whose behaviour of the components is described as a CSP process. Finally,
we introduce three case studies to evaluate 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.
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/22209 |
| Date | 12 August 2016 |
| Creators | Conserva Filho, Madiel de Souza |
| Contributors | 02386943488, http://lattes.cnpq.br/1756952696097255, Mota, Alexandre Cabral, 73547735491, http://lattes.cnpq.br/2794026545404598, Moreira, Anamaria Martins, 82573611787, http://lattes.cnpq.br/2363575151206774, Ribeiro, Leila, 50881884049, Musicante, Martin Alejandro, 82500304434, http://lattes.cnpq.br/6034405930958244, Cavalcanti, Ana Lucia Caneca, 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/doctoralThesis |
| 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.0025 seconds