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.

Serviceevolution erlaubt es, einen Service durch einen anderen Service zu verfeinern oder zu ersetzen. Der Austausch durch einen anderen Service sollte garantieren, dass alle oder ausgewählte Partner des Originalservices erhalten bleiben. In dieser Arbeit entwickeln wir einen Ansatz welcher einem Serviceentwickler helfen soll, Analyse- und Syntheseaufgaben für den Serviceaustausch so durchzuführen, dass jeder Partner eines gegebenen Services beim Austausch erhalten bleibt. Wir modellieren einen Kontrollfluss eines Services als Beschreibung der Reihenfolge von asynchron kommunizierenden Ereignissen mittels eines impliziten ungeordneten Nachrichtenspeichers. Weiterhin studieren wir den Verhaltensaspekt von korrekter Interaktion zwischen Services und konzentrieren uns auf zwei Varianten von Verklemmungsfreiheit als Korrektheitskriterien von Serviceersetzung. Der wichtigste Beitrag ist ein Ansatz zur Charakterisierung jedes möglichen Austausches eines gegebenen Services. Die zentrale Idee dieses Ansatzes ist eine systematische Untersuchung der Verbindung zwischen einem Service und all seiner Partner bzgl. eines gegebenen Korrektheitskriteriums. Wir nutzen diese Verbindung um von einem gegebenen Service einen kanonischen Partner und einen kanonischen Austausch bzgl. aller Partner zu synthetisieren. Ein Service welcher den kanonischen Austausch eines gegebenen Services verfeinert wird als Austausch des gegebenen Services angesehen, wenn die Menge all seiner Partner jeden Partner des gegebenen Services enthält. Mit dem kanonischen Austausch eines gegebenen Services identifizieren wir die Menge der möglichen austauschenden Services eines gegebenen Services bei der jeder exakt die gleichen Partner wie der gegebene Service hat. Einige Ergebnisse dieser Arbeit fundieren auf früheren Arbeiten zu Austausch und Korrektheit von Services und können daher mit diesen verbunden werden um schwierigere Analyse- und Syntheseaufgaben für den Serviceaustausch durchzuführen. / Service evolution allows one service to be refined into or substituted by another service. Substituting one service by another service should guarantee to preserve all or selected partners of the original service. In this thesis, we develop an approach that shall assist a service designer, such as a domain expert, to perform analysis and synthesis tasks on service substitution. We model a control flow of services that describes the ordering of asynchronously communicating events over an implicit unordered message buffer. We study the behavioral aspect of correct interaction between services and concentrate on two variants of deadlock freedom as correctness criteria of service substitution. The major contribution of this thesis is an approach for characterizing the set of all substitutes for a given service. We systematically investigate the relationship between a service and all its partners under a given correctness criterion and employ this relationship to synthesize from a given service its canonical partner and its canonical substitute with respect to all partners. A service that refines the canonical substitute for a given service is regarded as a substitute for the given service if the set of all its partners includes every partner of the given service. With the canonical substitute of a given service, we identify a specific subset of the set of all substitutes for the given service, each of which has exactly the same set of partners as that of the given service. Parts of the results in this thesis have been established upon previous works on service substitution and correctness of services. Consequently, we can also combine our results with the related existing techniques to perform more sophisticated analysis and synthesis tasks on service substitution.