Utilize este identificador para referenciar este registo: http://hdl.handle.net/10451/15862
Título: Tools and techniques for the static verification of progress in communication-centred systems
Autor: Camacho, André Filipe Marinhas Henriques da Silva
Orientador: Vasconcelos, Vasco Thudichum, 1964-
Vieira, Hugo Filipe Mendes Torres
Palavras-chave: Verificação de software
Sistema de tipos
Fidelidade
Progresso
Concorrência
Teses de mestrado - 2014
Data de Defesa: 2014
Resumo: Com a crescente disseminação da computação distribuída nos últimos anos, a forma como prevenimos os erros de programas concorrentes é cada vez mais importante. O desenvolvimento de programas concorrentes é difícil, exigindo ao programador um grande esforço para tentar “prever” possíveis estados futuros do programa. Num sistema concorrente a execução¸ ˜ao pode ter um amplo número de caminhos possíveis cujo resultado pode ser inesperado. Mesmo realizando intensivos testes de software, pode-se nunca chegar a explorar a sequência necessária para encontrar os caminhos que levam a certos erros, tornando estes testes insuficientes. Um dos erros difíceis de detetar ´e a ocorrência de pontos de bloqueio, designados por deadlocks. Um sistema possui a propriedade de progresso, quando na sua execução¸ ao não ocorrem pontos de bloqueio. É necessário provar que nenhum caminho possível revela surpresas, para garantir que existe progresso no sistema. A nossa abordagem procura garantir a ausência de pontos de bloqueio, para além de outras propriedades de correção, implementando técnicas de verificação a serem usadas em ferramentas de análise estática (apenas inspecionando o código fonte). A verificação vai ser realizada em sistemas concorrentes baseados em troca de mensagens, onde vão ser garantidas as propriedades de fidelidade e progresso. Garantindo estas propriedades é possível ter a certeza que as mensagens trocadas seguem um protocolo bem definido e que o sistema está livre de pontos de bloqueio. A linguagem de modelação de sistemas usada no contexto deste trabalho é baseada no calculo π introduzido por Milner, Parrow e Walker [5, 6], um modelo universal de computação que permite modelar e especificar de uma forma precisa sistemas de processos concorrentes, servindo posteriormente de suporte para técnicas rigorosas de análise de propriedades. Para garantir a propriedade de progresso vai ser usado um sistema de tipos que unifica a noção de evento com os tipos de sessão introduzido por Honda, Kubo e Vasconcelos [2, 3] que permitem descrever o protocolo de comunicação entre dois participantes pontoa- ponto. O uso da noção de evento introduzido por Vieira e Vasconcelos [9], permite capturar as dependências das comunicações entre processos e suporta a verificação que estas estão bem estruturadas. Como objetivo, vão ser endereçadas comunicações ponto-a-ponto sendo-nos dadas as especificações dos tipos (incluindo as anotações de eventos) e a ordenação de eventos, por forma a conferir se o programa está de acordo com as especificações.
With the growing dissemination of distributed computing in recent years, preventing runtime errors in concurrent programs is increasingly important. The development of concurrent programs is difficult, requiring from the programmer a great effort to “predict” possible future states of the program. In a concurrent system the execution can have a large number of possible paths, some of which leading to unexpected behaviours. Even performing intensive software testing, the explored sequence may never find the paths that lead to certain errors, making such testing incomplete. Deadlocks are one of the hard to detect errors in concurrent systems. We say that a system has the property of progress when its execution does not lead to deadlocks. It is necessary to prove that no path reveals any surprises to ensure that there is progress in the system. Our approach aims to ensure the absence of deadlocks in addition to other correctness properties, implementing verification techniques to be used in static analysis tools (that just inspect the source code). The analysis will be performed on concurrent systems based on message exchanges, targeting the properties of fidelity and progress. Ensuring such properties means guaranteeing that the message exchanges follow a well-defined protocol and that the system is free from deadlocks. The language used to model systems in the context of this work is based on the π- Calculus introduced by Milner, Parrow and Walker [5, 6], a universal model of computation which allows to model and specify concurrent systems in a precise way, serving subsequently as a support for rigorous analysis techniques. To ensure progress, we will use a type system that unifies a notion of event with the session types introduced by Honda, Kubo and Vasconcelos [2, 3] which allow to describe the communication protocol between two participants (point-to-point). The use of events introduce by Vieira and Vasconcelos [9], allows to capture the communication dependencies between processes so as to support the verification that such dependencies are well structured. Our goal will be to support point-to-point communications, considering the type specifications (including the event annotations) and the orderings of events are given, which allow us to check if the program is in accordance with the specifications.
Descrição: Tese de mestrado, Engenharia Informática (Engenharia de Software), Universidade de Lisboa, Faculdade de Ciências, 2014
URI: http://hdl.handle.net/10451/15862
Designação: Mestrado em Engenharia Informática (Engenharia de Software)
Aparece nas colecções:FC-DI - Master Thesis (dissertation)

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
ulfc112332_tm_André_Camacho.pdf661,15 kBAdobe PDFVer/Abrir


FacebookTwitterDeliciousLinkedInDiggGoogle BookmarksMySpace
Formato BibTex MendeleyEndnote Degois 

Todos os registos no repositório estão protegidos por leis de copyright, com todos os direitos reservados.