| dc.contributor | SAMPAIO, Augusto Cezar Alves | |
| dc.creator | ANTONINO, Pedro Ribeiro Gonçalves | |
| dc.date | 2015-03-11T17:34:41Z | |
| dc.date | 2015-03-11T17:34:41Z | |
| dc.date | 2014-03-31 | |
| dc.identifier | ANTONINO, Pedro Ribeiro Gonçalves. A refinement based strategy for locally verifying networks of CSP processes. Recife, 2014. 150 f. Dissertação (mestrado) - UFPE, Centro de Informática, Programa de Pós-graduação em Ciência da Computação, 2013. | |
| dc.identifier | https://repositorio.ufpe.br/handle/123456789/11966 | |
| dc.description | 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. | |
| dc.description | 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. | |
| dc.format | application/pdf | |
| dc.language | eng | |
| dc.publisher | Universidade Federal de Pernambuco | |
| dc.rights | Attribution-NonCommercial-NoDerivs 3.0 Brazil | |
| dc.rights | http://creativecommons.org/licenses/by-nc-nd/3.0/br/ | |
| dc.subject | Ausência de deadlocks | |
| dc.subject | CSP | |
| dc.subject | FDR | |
| dc.subject | Análise local | |
| dc.subject | Verificação de modelos | |
| dc.subject | Deadlock freedom | |
| dc.subject | Local analysis | |
| dc.subject | Model checking | |
| dc.title | A refinement based strategy for locally verifying networks of CSP processes | |
| dc.type | masterThesis | |
