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.