Dissertação

Spatial Types for Concurrency: A Spatial Logic to Specify and Verify Distributed Systems A Spatial Logic to Specify and Verify Distributed Systems EVALUATED

Na ciência da computação, especificar e verificar propriedades comportamentais é considerado um problema clássico. Recentemente, tem surgido um interesse em propriedades espaciais de processos em sistemas distribuídos. Como tal, têm sido propostas lógicas modais cujos sistemas de prova são, em geral, indecidíveis. Uma excepção é o provador automático proposto por Luís Caires. Tradicionalmente, os sistemas de tipos são usados para garantir ausência de erros em linguagens de programação por serem decidíveis e de complexidade reduzida, mas recentemente, também têm sido usados para garantir propriedades espaciais de processos. O objectivo desta tese é definir uma lógica decidível (sintaxe, semântica e sistema dedutivo) que permita especificar e verificar estaticamente propriedades, nomeadamente invariantes, não só espaciais como comportamentais, em sistemas distribuídos implementados através de processos concorrentes. Neste trabalho, começa-se por escolher uma linguagem simples de processos e uma linguagem expressiva de fórmulas. A primeira é o fragmento livre de escolha não-determinística do CCS de Milner enquanto que a segunda baseia-se na Lógica Espacial de Caires e Cardelli e na Lógica de Processos de Milner. Adoptando a abordagem ?proposições como tipos?, estabelece-se uma semântica denotacional, baseada em relações estruturais e de transição, e uma noção de subtipagem, interpretada como implicação lógica. De seguida, define-se como sistema dedutivo um sistema de tipos e prova-se alguns resultados que o caracterizam, nomeadamente um resultado de consistência fraca e um resultado de completude. Por último, desenvolve-se uma aplicação que consiste em derivar uma asserção no sistema e que permite observar o seu potencial.
Álgebra de Processos, Concorrente, Comportamental, Lógica Espacial, Tipo, Sistema de Tipos

Outubro 9, 2007, 9:0

Publicação

Obra sujeita a Direitos de Autor

Orientação

ORIENTADOR

António Maria Alarcão Ravara

Departamento de Matemática (DM)

Professor Auxiliar