The increase of computer systems complexity has led to a direct increase in the difficulty of verifying their correctness. For mastering this complexity, formal methods can be used in the development of systems providing techniques for both design and verification. Regarding concurrent and distributed systems, the necessity of a formal approach is more prominent given the substantial increase in complexity due to the countless number of interactions between their constituent systems. Unfortunately, however, current methods are not capable of dealing with the automated analysis of such systems in general, even if we consider only classical properties such as deadlock freedom; the state explosion problem is the main reason for this ineffectiveness. This work is a contribution in this direction. Particularly, considering networks of CSP processes, this work proposes a local strategy for deadlock analysis based on the notion of process refinement. The locality of this strategy prevents the state explosion problem generated by the interaction of constituent systems, which represents a major asset of our strategy. We define a refinement assertion for checking conflict freedom between pairs of processes in the network; this can be used for the local verification of networks with an acyclic communication topology. Concerning networks with a cyclic communication topology, we propose three patterns that prevent deadlocks: the resource allocation, the client/server and the async dynamic. These patterns impose behavioural and structural restrictions to prevent deadlocks. The behavioural restrictions are also captured by refinement assertions, which enable one to automatically verify these conditions using a refinement checker. Besides this, we develop four case studies to evaluate the efficiency of our strategy in practice: a ring buffer, a dining philosopher, and two variations of a leadership election algorithm. One of the variations of the leadership election algorithm consists of a model used in practice by the B&O Company, an industrial partner. In this study, we compare our strategy with two other techniques for deadlock freedom verification, the SSD algorithm of the Deadlock Checker tool and the built-in deadlock freedom assertion of FDR. This study demonstrates how our strategy can be used and that it might be a useful alternative to analysing complex industrial systems for deadlock freedom. / Submitted by Luiz Felipe Barbosa (luiz.fbabreu2@ufpe.br) on 2015-03-10T16:54:41Z No. of bitstreams: 2 DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) / Made available in DSpace on 2015-03-11T17:34:41Z (GMT). No. of bitstreams: 2 DISSERTAÇÃO Pedro Ribeiro Gonçalves Antônio.pdf: 921372 bytes, checksum: 64def1c3ae98cbca7868d944c1f786f2 (MD5) license_rdf: 1232 bytes, checksum: 66e71c371cc565284e70f40736c94386 (MD5) Previous issue date: 2014-03-31 / Com o aumento da complexidade dos sistemas computacionais, houve também um aumento da dificuldade na tarefa de verificação de sistemas. Para lidar com essa complexidade, métodos formais podem ser usados no desenvolvimento de sistemas, fornecendo técnicas para a modelagem e verificação. No contexto de sistemas concorrentes e distribuídos, a necessidade de uma abordagem formal é ainda mais proeminente, dadas as inúmeras possibilidades de interação entre seus sistemas componentes. Entretanto, infelizmente, os métodos atuais não se encontram, de forma geral, completamente aptos a lidar com a análise automática desses sistemas, mesmo em se tratando de propriedades clássicas como a ausência de deadlocks. A explosão do espaço de estados a ser analisado é o principal fator para essa ineficácia por parte desses sistemas. O trabalho apresentado é uma contribuição nesta direção. Considerando o conceito de redes de processos CSP, o presente trabalho propõe uma estratégia local para a análise de deadlocks baseada na noção de refinamento de processos. A localidade dessa estratégia previne a explosão de espaço de estados causada pela interação de sistemas componentes, o que constitui uma vantajosa característica da nossa estratégia. O trabalho define uma expressão de refinamento capturando o conceito de ausência de conflito, que pode ser usado para verificar localmente que uma rede de processos com uma topologia de comunicação acíclica é livre de deadlocks. Para as redes com topologia cíclica, o trabalho sistematiza e formaliza três padrões comportamentais que impedem deadlocks: o alocação de recursos, o cliente/servidor e o assíncrono dinâmico. Esses padrões impõem restrições comportamentais e estruturais para prevenir deadlocks. Essas restrições comportamentais também são capturadas através de expressões de refinamento, o que possibilita a verificação automática dessas condições com o uso de um verificador de refinamento. Além disso, são apresentados quatro estudos de caso usados para avaliar o desempenho da nossa técnica na prática: um buffer circular, um jantar dos filósofos e duas variações de um algoritmo para eleição de líder. Uma dessas variações consiste num modelo usado na prática pela empresa B&O, um parceiro industrial. Nesse estudo, avaliamos a nossa técnica em comparação com outras duas técnicas para verificação de ausência de deadlocks, o algoritmo SSD da ferramenta Deadlock Checker e a asserção de verificação de deadlocks padrão do verificador de modelos FDR. Esse estudo demonstra como a nossa estratégia é aplicada e que ela pode ser uma alternativa vantajosa para a verificação de sistemas complexos.